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 model-oriented 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 

Elem

]

then

local 

pred

is_sorted	:  List[Elem];

var

L : List[Elem]

.

%[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

L	:  List[Elem];
x	:  Elem

.

%[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 well-known 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¹, 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 

Elem;

]

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

L	:  List[Elem];
x	:  Elem

.

%[mergesort_def1]  mergesort[__ < __]([])  =  []

end