[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Methodology Task Group - plans, meeting
CoFI Task Group on Methodology
Minutes of the Tarquinia meeting
Saturday, May 31st (afternoon) and Sunday, June 1st (morning)
Contents:
---------
I - List of participants
II - Summary of discussions
III - Work to be done
*******************************************************************************
* I - List of participants
*******************************************************************************
Hubert Baumeister (HB)
Michel Bidoit (MB), Chair.
Christine Choppy (CC)
Bernd Krieg-Brueckner (BKB)
Gianna Reggio (GR)
Don Sannella (DS)
Andrzej Tarlecki (AT)
Peter Mosses was pretending not attending the meeting, but was sitting
closely enough to hear what was going on :-)
I have forgotten to take note of the people attending the meeting; my
sincere apologies to omitted people, if any.
*******************************************************************************
* II - Summary of discussions
*******************************************************************************
a) MB starts by recalling the general aims and scope of this Task Group:
Aims and Scope:
===============
The aim of the Methodology task group is to enrich the formalism designed
under the Common Framework Initiative with ideas on the methodology of
system specification and development that we would like to support,
encourage and propagate. We intend to influence the overall design of the
formalism to support these methodological views.
We plan to address methodological issues arising throughout the software
development life cycle. For instance:
* the role of specifications in the development process (relationship
between specifications and programs, formal vs. semi-formal specifications);
* an abstract view of the development process (refinement and proof
obligations, design specifications in-the-large and structuring issues,
behavioural interpretation of specifications, reusability of
modules/specifications/developments, flexibility and evolution);
* techniques for writing specifications of individual system modules
(algebraic specifications vs. other specification techniques,
reachability/initiality, verifying specifications via theorem proving,
testing, checking completeness properties).
The expected outcome is a proposal for how a naive user should proceed with
the development of a simple system, propped up by a number of more advanced
methods which we believe would be useful in the context of more complex
systems and/or when larger development teams are involved. We also would
like to present these ideas to the user in a readable and self-contained
document.
b) Moreover, during the last (very short) meeting of the CoFI Task Group on
Methodology in Edinburgh last november, the following issues have been
proposed:
XL (Extra large):
Role of algebraic (axiomatic) specifications in software
engineering. E.g. requirements engineering (from informal requirements to
formal requirements), formal vs. semi-formal specifications, applications to
software testing, software reuse, software reverse engineering.
Relationship between specifications and programs.
Reusability of specifications, of developments.
L (Large):
Formal software development: from a formal requirements
specification to a formal design specification and then possibly a program
written in some existing programming language. Role of architectural
specifications. Behavioural refinement.
S (Small):
How to use the various features of the language. E.g. partial
functions vs. total functions on subsorts, generic specifications,
architectural specifications. How to avoid misusing the language constructs
(e.g. existential equality vs. strong equality). Guidelines for writing
individual pieces of specifications, for structuring large specifications.
CASL Tutorial
Illustrative examples
Case studies
c) After a general discussion and global agreement on the issues listed
above, it is decided to focus on ``in the small'' issues first. For this,
there are two approaches: on a construct per construct basis, or on a more
``problem-oriented'' basis. It is agreed that the second approach is more
meaningful. However, to help the group to identify relevant topics, it is
decided to start by a ``construct per construct'' approach. It is also
decided to try and identify specific specification styles, possibly
associated with some CASL sub-languages. The list of issues discussed is
given below:
(i) How to define a datatype ?
(ii) Predicates versus boolean functions
(iii) Partial functions:
* definedness
* strong/existential equality
* impact of strictness ( f(a) defined implies a defined ! )
* partiality versus abstraction level/underspecification
e.g. f(x) is defined iff/when
looseness simulated by partiality
(iv) Partiality and predicates:
* Predicates are ``strict'', i.e. yield false on undefined
arguments...
* Explain the impact for axioms, negation, etc.
Undef (x) <=> not(x is_defined) has not the ``expected''
meaning, since not(Pred(t)) is true when t is undefined...
Similarly, if Pred(...) then ... else ... is misleading,
or at least misinterpretable, e.g.:
if 1/x > 0 then 5 else 6 will ``yield'' 6 for x=0
(v) Predicates:
* Undefined arguments (see iv)
* Versus boolean functions (see ii)
* Least fixed point in conjunction with freeness
* How to use predicates to better structure formulas,
auxiliary definitions etc.
(vi) Variable declarations:
* Empty carrier: initial model not always exists...
* Do not contribute to the exported signature
* owerwriting, overriding, etc: don't use it, even when
allowed ...
* Let z = term in formula
(vii) Datatype declaration:
* loose / generated / freely generated
* Examples and explanations are needed
* Advices for choosing between the three cases above...
(see i)
(viii) Axioms:
* 2-valued, difference between /\ (logical connective) and
the user-defined boolean function ``and''
* Do not use boolean operators !? What do we loose by not
having a three-valued logic ? (cf. e.g. Oslo group).
* How to ``find'' the axioms to be written ?
* Various styles for writing axioms
* When to state attributes (e.g. commutativity) as FUN-ATTR
or as plain axioms
* Writing true property-oriented specifications versus
almost programs (recursive definitions)
* Conditional equations: danger w.r.t. strong/existential
equality...
(ix) Sort generation:
* Recommended use of inductive techniques
* multiple versus single sort generation (danger)
* difference between generation constraints and freeness
(cf. vii)
* cannot be simulated by 1st order formula
(x) Hiding: use of local declarations versus revealing/hiding
(xi) Subsorts:
* Various kinds of subsorts (e.g. subsorts for subtypes,
ranges)
* Datatype defined as alternative of subsorts
* Implicit versus explicit subsorts,
constructive/predicative/implicit subsort
* Use of subsort to get the effect of disjoint union
* loose datatype definition with subsorts
* Definition of CASL Abstract Syntax as an example
* Potential misuse of subsorts
* How to overload in order to get the desired effect ?
* Why to name subsorts:
Stack = empty | push(Elem, Stack)
vs Stack = EmptyStack | NonEmptyStack
Warning: either partial selectors or cast !
* How to avoid the use of subsorts: style advocating the
use of subsorts, style advocating not to use subsorts
* Reachability construct/freeness/initiality in the
presence of subsorts
* Iso-decls
* Embeddings versus inclusions (Int < Real)
* Bad subsort declarations e.g. Elem < List[Elem]
(xii) Role of structuring concepts w.r.t. specification reuse
(xiii) Different aims of structured specifications and architectural
specifications
(xiv) Impact of splitting in various pieces when using architectural
specifications
(xv) Various concepts of refinement
(refinement/implementation/realization or reification)
* Clarification of terminology is needed
(xvi) renaming/hiding in relation with name clashes
(xvii) Hiding: three levels
* local item/spec
* hiding
* in architectural spec
(xviii) Extension:
* How big is the extension ?
* How often to name a subspecification
* Granularity of specification expressions
* Why union AND extension ?
* Role of conservative extension
(xix) Freeness:
* How to avoid the use of free extensions
by providing enough observers
* When are free extensions useful ?
* Freeness: how to use it ? Consequences for axioms
(xx) Union: decomposition of specifications into independant pieces, cf
sharing
(xxi) Generic specifications:
* Difference between generic spec and architectural spec
* How to write meaningful generic spec
* pushout style versus lambda/ASL/parametric style
* positional instantiation
* Compound identifiers
(xxii) Architectural specifications:
* Explanation with convincing examples
* Reusability of programs rather than specs
* Interfaces
* Different constructs at the struct spec level and the
arch spec level
* sharing
* relation with code
(xxiii) Distributed libraries/Downloading
* Version control ?
--------------------------------------------------------------
The list of issues above is to be kept in mind. In a first step, it is
decided to write a few notes on some important topics, cf. below.
*******************************************************************************
* III - Work to be done
*******************************************************************************
Here is the list of notes to be written:
(A) Note discussing refinement and the role of architectural
specifications (and possibly the role of other constructs)
AT (+ DS + MB)
(B) Note on generic specifications
MB (+ GR)
(C) Note on partiality
GR (+ Martin Wirsing)
(D) Note on subsorts (how to avoid partiality with subsorts)
BKB (+ Anne Haxthausen + Olaf)
(E) Note on various kinds of subsorts
Maura Cerioli
(F) Note on predicates (versus boolean functions - least fixed point -
partiality)
GR
(G) Note on initiality and freeness
GR
(H) Note on datatype definitions
CC
(I) Note on union and extension (and granularity of struct. spec)
HB (+ MB)
(J) Note on encapsulation, hiding (3 levels)
MB
(K) Note on libraries
PM (+BKB)
Important:
==========
* The notes should reflect the discussion (e.g. points (i) to (xxiii))
* The notes should be written using the cofidoc.sty package
* The notes should provide relevant examples in concrete syntax
* The notes should be kept concise (5 to 10 pages)
* The notes should be written using the style used by Peter Mosses
in his Tapsoft paper. This helps in designing the note (cf. the
quote convention).
A first sketch of the notes (at least detailed intended content) is to be
circulated on the methodology list by SEPTEMBER 11th, 1997.