How to write consistent CASL design specifications
Till Mossakowski
March 2000
This document is available by
FTP
in various formats.
It was converted to HTML using
Hyperlatex 2.3.
Abstract
We emphasize the role of consistency
in the development process and in particular the
need to write consistent design specifications.
CASL takes an axiomatic approach, as opposed to
modeloriented approaches like VDM or Z.
This means that it is possible to specify
loose requirements at a very high level.
Moreover, it is possible to decribe abstract data
types only w.r.t. their properties, without
giving any intended implementation.
Consider e.g. the following requirement specification of
sorting lists:
from Basic/RelationsAndOrders get
TotalOrder
from Basic/StructuredDatatypes get
List
 spec
 Sort
[TotalOrder] =

List [sort
]
 then
 local
 pred

 var

 .

%[is_sorted_def] is_sorted( L) <=> 
(forall K,K':List[Elem]; x,y:Elem · 
L = K++(x::nil)++(y::nil)++K'
=> x < y )

 within

 op

sorter[__ < __]  :  List[Elem] > List[Elem]; 

 vars

 .

%[sorter1] x eps L <=> x eps sorter[__ < __]( L) 
 .

%[sorter2] is_sorted(sorter[__ < __]( L)) 
 end
The specification is not concerned with any
implementation details. The strength of this
approach is that it is near to the informal
requirements, so it is much easier to validate
the specification, i.e. check if it is
a correct formalization of what is inteded
of informally specified.
We can summarize this:
Within requirement specifications, axioms are useful.
However, a danger of this approach is that the
requirement specification is inconsistent.
Indeed, at the requirement specification level,
it is a deliberately chosen risk to introduce
inconsistencies, and in many cases, it will happen
that the specification contains some inconsistencies,
which have to be eliminated during the development
process.
Now proving consistency of a specification is
hard. With theorem proving, it is possible
to find inconsistencies: A specification
is inconsistent if and only if it is possible
to derive false from it. However, in general
theorem proving is not capable of
proving a specification to be consistent.
Thus the only way to check consistency is to
refine the specification until it lives
in a formalism that allows to express only
consistent specifications. Of course, this
stage is reached if there is a em program
that implements the given specification:
a program is by definition consistent,
and (with the right notion of refinement)
it leads to a model of the original specification,
proving its consistency.
However, the refinement of a specification into
a program is a costly process, and therefore
consistency of a specifiation should be checked
as early as possible, since an inconsistency
will lead to a revision of the requirement specification,
and the development process has to be redone.
The wellknown solution is to introcude a level of
design specifications that model
the data structures and algorithms
that are used to implement the requirement
specification, but without being cluttered
with the details of a real program.
Now a design specification em should
be consistent. Thus, it is harmful
to arbitrarily introduce axioms into
a design specification  each new axiom
may lead to new inconsistencies. In a word,
Within design specifications, axioms are harmful.
Instead of writing arbitrary axioms,
one should write axioms (and specifications)
in a form that guarantees their consistency.
Thus, we look for a sublanguage of CASL that is
 as powerful as possible, but
 still recognizable in reasonable time^{1}, and
 guaranteed to be consistent.
The sublanguage should at least cover:
 free datatypes
 primitive recursive functions and predicates defined over free datatypes
 mutual recursion over mutually recursive free datatypes
 distinction by (mutually disjoint and jointly exhaustive) cases
Some first attempt to formulate such rules for a sublanguage
in this direction have been made in
[RM99] and [Mos98].
The sublanguage should be worked out more properly and also
supported with tools recognizing the
consistent sublanguage.
When writing the CASL basic datatypes [RM00],
we largely have followed rules for writing consistent design
specifications, since concerning basic datatypes,
their consistency is a very important issue.
Of course, it is also important that the basic
datatypes meet the abstract requirements that one expects
them to meet; this is expressed in [RM00]
via views going from requirement to design specifications.
As a small example, consider
the following design specification of merge sort.
With a sublanguage for consistent design specifications,
it should be possible to automatically check it to be consistent.
 spec
 Mergesort
[TotalOrder] =

List [sort
]
 then
 local
 ops

merge  :  List[Elem] × List[Elem] > List[Elem]; 
get_odds, get_evens  :  List[Elem] > List[Elem]; 


 vars

K, L  : List[Elem]; 
x, y  : Elem 

 .

%[merge_def1] merge( [] , L ) = L 
 .

%[merge_def2] merge( L , [] ) = L 
 .

%[merge_def3] merge(x::L,y::K) = x::merge(L,y::K) if x < y 
 .

%[merge_def4] merge(x::L,y::K) = y::merge(x::L,K) if ¬ x < y 
 .

%[get_odds_def1] get_odds([]) = [] 
 .

%[get_odds_def2] get_odds(x::L) = x::get_evens(L) 
 .

%[get_evens_def1] get_evens([]) = [] 
 .

%[get_evens_def2] get_evens(x::L) = get_odds(L) 
 within

 op

mergesort[__ < __]  :  List[Elem] > List[Elem]; 

 vars

 .

%[mergesort_def1] mergesort[__ < __]([]) = [] 
 end
CoFI
Note: M8  Version: 1.0  March 2000.
Comments to till@informatik.unibremen.de