MSc Project Report

The recently developed algebraic specification language CASL is intended to be a standard in the field. This project is concerned with providing theorem proving support for CASL by writing a tool to translate CASL basic specifications for use with the commercially and academically proven verification system PVS.

Above all I wish to thank my supervisor, Don Sannella, for proposing an interesting and challenging project, for unfailing guidance in carrying it out and continuous reassurance in the face of the author’s increasing panic.

I would also like to thank Paul Jackson for advice on PVS, Till Mossakowski and the University of Bremen CoFI group for their parser and advice on using it and Mark van den Brand and Pieter Olivier for advice on the Java ATerm library.

Finally I would like to thank my father for the use of his study and his PC (on which this was written) and the University of Edinburgh Division of Informatics for all the other facilities used in this project and for accepting me to do the MSc. course in the first place.

1. Introduction

1.1 Background

1.2 Work Done

1.3 Previous Work

1.4 The Report

2. CASL

2.1 Basic Specifications

2.2 The Other Parts of CASL

3. PVS

3.1 The Language

3.2 The Prover

4. Translation of CASL to PVS

4.1 Signature Items

4.2 Other Items

5. The Implementation

6. Conclusion and Further Work

Bibliography

Appendix

In algebraic specification a program is modelled as a description of sets of data values (called sorts or types) and functions over these collections. The behaviour of a program is then described by adding axioms constraining the properties of the functions.

Of the many algebraic specification languages available none has achieved wide use. So, since 1995 CoFI, the Common Framework Initiative, which is an international collaboration aiming to develop a standard for algebraic specification, has been developing CASL, the Common Algebraic Specification Language, which, it is hoped, will become a standard for algebraic specification since it incorporates the best features of a range of other such languages [San99].

There already exist a wide variety of tools, parsers, type checkers, provers, etc for other specification languages so it is proposed in [BKO98] that pre-existing tools should be adapted for use with CASL rather than being written specially. So the object of this project is to provide theorem proving support for the core CASL language by developing a tool that converts CASL specifications for use with the PVS theorem prover.

PVS (Prototype Verification System), developed by SRI International, is a specification language fully integrated with a parser, a type-checker and a powerful theorem prover. It has been designed to be easy to use and has been widely used in industry as well as academia. The specification language uses a simply typed higher-order logic that only admits total functions, but which includes a powerful subtyping mechanism [OSRS98a].

The goal of the project was to write a tool that translated CASL specifications into PVS theories. Since PVS only admits total functions I started by restricting the specifications considered by excluding those with partial functions. Further restrictions proved necessary because of the different ways CASL and PVS dealt with subtyping. The tool was firstly to deal with basic specifications and then move on to the more complicated, structured specifications. As it turned out I was able to translate almost all the constructs in basic specifications, but shortage of time prevented me moving on to structured specifications. The implementation I have produced is a prototype that builds on PVS and a pre-existing CASL parser, but does not integrate these components into one system.

Previously in this area work has been carried out to support theorem proving in CASL by embedding it in the Isabelle theorem prover [MKKB98]. Also the inka 5.0 system, which is a theorem prover with a specification language, has been designed to include a subset of CASL within its language [AHMS99].

Following chapters will describe CASL and then PVS. After that I will describe the details of my translation from CASL basic specifications to PVS, then the implementation itself, with examples. Finally I will sum up my work and consider how it could be further developed.

CASL comes in four parts: basic specifications, which contain simple declarations, definitions and axioms; structured specifications, for combining basic specifications; architectural specifications, for specifying the modular structure of the specified system and libraries of reusable specifications. A full description of CASL can be found in [COFI98], with introductions in [Mos99] and [San99].

Basic specifications, which I will be considering in this project, consist of a signature and sentences, or axioms, constraining the properties of the elements of the signature.

A signature determines the sorts, operations and predicates of a specification. Simple sorts may be declared. Subsorts may be simply declared, e.g.

declares s as a subsort of t. Or subsets may be defined as follows :-

which declares s as a subsort of t consisting of those values of t that satisfy the formula F. The subtyping relation between sorts is modelled by embeddings of subsorts into supersorts rather than set inclusion as in some other frameworks [CHKBM97]. This greater flexibility means that subsorts need not be assumed to have the same data representation as their supersorts, e.g. in integers and floating point decimals, which are represented differently for efficiency reasons, though the former may be taken as a subsort of the other.

Operations may be declared total or partial, e.g.

declares f as total from s into t and g as partial from s into t. Whether some term involving partial functions is defined can be asserted in a definedness formula. When a binary operation is declared it can be additionally declared to have any number of four standard attributes: commutativity, associativity, idempotency, or possession of a specified identity element.

A datatype declaration declares a sort with constructors and optional selectors (both may be total or partial) and determines sentences on these. E.g.:

determines a type of lists with elements belonging to s with two constructors and two partial selectors, hd and tl. A datatype declaration, as above, also asserts that the selectors give the expected values, e.g. that

and

for all lists t and elements of s h.

If a datatype is declared free then this also determines that the constructors are injective, that the ranges of the constructors are disjoint and cover the entire set and that the value of applying the selectors to values of constructors for which they have not been declared is always undefined. It is also possible to use a ‘subsort alternative’ to build a datatype from previously declared sorts without constructors and in free datatypes these sorts will have no common subsorts. Within a list of datatypes the order is not significant. This non-linear visibility allows the declaration of mutually recursive datatypes.

A sort generation constraint may be placed on a list of signature items indicating that the sorts declared are generated by the operations declared. I.e. there are no members of the sorts not in the range of some operation within the constraint, so an induction principle may be inferred.

In CASL operations may be declared using ‘mixfix’ notation, a system that generalises infix, postfix and prefix notation by allowing placeholders and tokens to be mixed together in the declaration of an operation, e.g.:

declares the binary operation ‘+’. Application of this operation to variables x and y may be written ‘x+y’, +(x,y) or ‘__+__(x,y)’. ‘Invisible’ identifiers consisting only of placeholders are permitted.

The sentences are written in first order logic with two kinds of equality for dealing with possibly undefined values. Given terms T and T', existential equality between them requires that T and T' are both defined and their values are equal. Strong equality requires that if T is defined then T' is defined and they have equal values and if T is not defined then T’ is not defined.

A model of the specification is an interpretation of the sorts, operations and predicates declared for which the sentences hold.

Structured specifications may build on basic specifications. Specifications may be named and made generic, so they can be instantiated with different parameters. Specifications may be joined together in unions. Specifications can be restricted by hiding elements (sorts, operations or predicates) or extended by adding elements. The models of a structured specification are the same as those of a basic specification. I.e. the structure of a specification is not reflected in its models, but is just meant to allow the presentation of a large specification to be broken into smaller pieces.

An architectural specification specifies the structure of a program. It gives a series of unit modules, which may be specified by basic or structured specifications, and a ‘unit term’, which indicates how the modules should fit together [BST99].

Finally libraries store collections of named specifications, either locally or in distributed libraries.

Each of the above parts of CASL is orthogonal to the others, which means they are independent and can be adapted without affecting the other parts [Mos99]. This means that CASL basic specifications may be easily restricted to sublanguages or extended to deal with specialised areas like concurrent systems without the other parts of CASL changing [San99].

Chapter 3

PVS (The Prototype Verification System) is a specification language smoothly integrated with a powerful theorem prover. It is implemented in LISP and works with a classical, higher order logic with total functions and a sophisticated, though undecidable, type system. The PVS system, language and prover are fully described in [OSRSC98a], [OSRSC98b] and [SORSC98].

A PVS specification is a collection of named theories. A theory consists of a signature specifying types and operations, axioms constraining these and theorems to be proved about them. It is possible for theories to import other theories and the theories to be imported can specify which elements of them are to be imported, so data hiding is possible. Theories can also be parameterised in specified types or values. Theories within a current directory form a context. For every theory PVS generates a proof file for storing proofs of theorems and for the context PVS generates a ‘.pvscontext file, which keeps track of which theorems have been proved.

All PVS theories implicitly include a built-in prelude, which includes the types ‘real’, ‘rational’, ‘integer’ and ‘naturalnumber’. New types can then be created by declaring new uninterpreted types (which may be empty unless specified non-empty) or using type constructors to create subtypes, function types, tuple types or record types. Subtypes may be declared using predicates, e.g.

So subtypes are interpreted simply as subsets of their supertypes.

Function, tuple and record types may be dependent in that some of the component types may depend on previous components.

The complexity of the type system means that it is in general undecidable. When a theory is typechecked PVS will typically produce type-correctness conditions (tccs). These are proof obligations that the user must prove before the theory is properly typechecked. For instance in the following theory extract:

where F is a formula containing the function op applied to x, PVS will produce the following tcc.

where S_pred is a predicate, automatically generated by PVS, such that

A special kind of type in PVS is the user defined abstract datatype. If a datatype is recursively defined it must be declared in a separate ‘Datatype’ theory, which may be parameterised. Datatypes are types declared with constructors, accessors and recognisers. E.g. a stack with elements of type t may be declared as follows:

This declares a type of stacks containing elements of some type t, constructors empty and push, accessors top and pop, and empty? and nonempty? as predicates for recognising which constructor a stack is constructed from. When this is typechecked PVS creates a theory called stack_adt containing all the relevant declarations, axioms asserting that two stacks with the same components (e.g. given by top and pop) are the same; that top and pop have the correct behaviour with respect to push; that empty? and nonempty? do not overlap and that the type of stacks is the union of empty? and nonempty?. Stack_adt then defines a large number of useful functions on stacks, including various ‘reduce’ functions, for use in creating measures for recursive functions (see below) along with an order on stacks and an axiom asserting that this order is well-founded. Stack_adt is included in full as an appendix.

‘Constants’ refers to functions and relations as well as 0-ary constants and these can be declared with or without giving a definition. If functions are recursive they must be declared as such with the keyword "RECURSIVE" and given a ‘measure’ function and an order relation (which defaults to the usual order on natural numbers or ordinals up to epsilon-0) to guarantee they terminate. When this is typechecked a type-correctness condition is generated requiring the user to prove that the measure strictly decreases with respect to the given order with every step in the recursion. E.g. in PVS one can define the factorial functions as follows [OSRSC98b]:

When typechecked this produces the following tcc:

Formulae are either axioms asserting properties of the specified constants or they are theorems giving desired properties to be proved.

The PVS prover is a powerful, interactive proof checker that has commands to carry out propositional, quantificational and equality reasoning easily. Proof commands can be combined to form strategies and new strategies can be written by the user. Proofs are stored and can be rerun or edited.

Chapter 4

The biggest difference between CASL basic specifications and PVS theories is that in CASL operations may be declared total or partial, while in PVS only total functions are permitted. Trying to reason about total functions is a lot easier than reasoning about partial functions, so a restriction to partial functions has practical benefits. In PVS partiality can be avoided by considering a subtype of the domain, e.g. division is partial on the real numbers, but total on the non-zero real numbers. Or one can think of a partial function f:Dà R as a total function f:Dà R' where R' is R with an extra element to denote 'undefined'. However, it was felt that to start off with, partial functions should be excluded from consideration. The exception to this rule is selectors or accessors of datatypes, which in most cases have to be partial over a datatype, e.g. in stacks, top and pop, which are only defined on non-empty stacks. To handle this subtypes of stack are introduced to turn top and pop into total functions.

The input into the program is an abstract representation of a basic specification, consisting of a list of ‘basic items’ which add to the signature, determine sentences or declare variables.

Most of the constructs in basic CASL specifications can be mapped directly onto PVS constructs. However, there are some subtle differences, which I shall deal with in turn.

4.1 Signature Items

Declarations that add to the signature are sorts, operations, predicates or datatypes. As a general rule in CASL items may be declared more than once, e.g. a sort may be declared as the subsort of more than one other sort. In PVS all items must be declared only once and additional information about items should be declared as axioms.

Sort declarations may be of uninterpreted sorts or subsorts, subsort definitions or isomorphism declarations. Sort declarations are exactly identical to declarations of uninterpreted types in PVS, but subsort declarations are subtly different. In PVS subtyping is modelled as simple set inclusion, while in CASL it is modelled as an embedding of the subsort into its supersort. As a result of this the subsort relationship can be much more complicated in CASL than in PVS. A sort can be a subsort of two non-overlapping supersorts, which is definitely not possible in PVS. Because of this the set of CASL specifications considered had to be restricted. In PVS it is not possible to declare a type as a subtype more than once to two different supertypes, although it is possible for a defined subtype to have the subtyping relationship to several non-equal supertypes by virtue of its definition. E.g.

where odd and prime are predicates on the integers. Here O and P are both defined as subtypes of the integers and OP is defined as a subtype of O, but is also a subtype of P by definition. If a function is applied to an element x of OP when it expects an element of P PVS generates a tcc (type-correctness condition) asking the user to prove that x is also of type P.

It is noted in [CHKBM97] that it is possible to pass from a model with embedded subsorts to an equivalent one with subsorts modelled as set inclusions, provided the subsorting relationship is "locally upward filtered". This means that any two sorts in the same locally connected part of the relation have a common supersort [GM92]. However, in view of the above a stronger condition must be placed on CASL specifications to be translated to PVS, namely that no subsort can be declared more than once to different supersorts.

PVS types may be empty, but can be declared to be non-empty. In CASL all sorts are non-empty, so in translation to PVS all sorts are converted to non-empty types.

An isomorphism declaration declares a series of distinct sorts, all subsorts of each other, implying they all have isomorphic interpretations. In translation to PVS one of these is declared as an uninterpreted type and the rest defined as equal to the first. This is okay provided none of these is then declared to be a subsort of some other sort without the others being so as well. This accords with the principle above of not declaring items more than once.

CASL datatypes concisely define a sort along with constructor and optional accessor functions. E.g:

declares stacks with elements containing of s with empty and push as constructors and pop and stack as partial accessors and also declares sentences ensuring that the selectors behave appropriately with respect to the constructors. E.g. from the example above we have,

and

In datatypes selectors are usually partial. In translation the type is declared. Then one subtype is declared for each constructor corresponding to the set of values produced by the constructor. Then the constructors and the selectors are declared and finally the appropriate sentences declared as axioms. E.g. the stack above translates to:

In the above ‘TYPE+’ indicates that types must be non-empty. stackcons1? and stackcons2? are subtypes of stack and are required to make the selectors push and pop total. The subsort alternative of datatypes is not supported because it declares new information about sorts already declared in the local environment. However, this could conceivably be handled by explicitly declaring injection functions to embed the subsorts into the type.

If a selector is declared total, and so declared for each alternative, this is equivalent to declaring overloaded selectors, each with a domain corresponding to a different subtype of the datatype. So, partial and total selectors are translated equivalently.

Datatypes declared as free determine the same sorts, operations and axioms as non-free datatypes and additional axioms further constraining the properties of the datatype. In fact CASL free datatypes are very similar to the PVS datatype construct so the translation makes direct use of this to translate PVS datatypes. E.g.

is translated in the main theory to

Then an additional file is created called stack.pvs, which contains the following:

When this is typechecked the file ‘stack_adt.pvs’ is created by PVS as described in chapter 3 and the contents of this are imported into the main theory. In PVS accessors (selectors in CASL) must be declared for every argument of every constructor so if some selectors are absent in the CASL specification they are automatically declared when the specification is translated. Here stackcons1? and stackcons2?, called recognisers in PVS are predicates, defining subtypes of stack implicitly. Again the subsort alternative is not handled because it does not fit in with PVS datatypes.

Additionally, for each datatype a ‘measure’ function is constructed to deal with recursive operations, as described below.

Again, partial and total selectors are translated identically, as described above.

In CASL a list of datatypes, free or non-free, can have non-linear visibility, allowing for mutually recursive datatype definitions. In PVS all visibility is strictly linear, so mutually recursive datatypes are not explicitly supported, although [OSRSC98b] suggests how this can be achieved in most typical cases by defining the datatypes together as one datatype with ‘subdatatypes’. The translation could possibly be adapted to achieve this.

Declarations and definitions of operations are almost exactly similar in PVS and CASL. The exception is recursive operations. In CASL recursive operations need not be declared as such, but in PVS they must be declared, using the keyword ‘RECURSIVE’. Then a ‘measure’ function must be given to ensure the function terminates and hence is total. A measure function must have the same profile as the recursive function, but with its range of the same type as the domain of the order. CASL has no built in types, so well-founded recursive functions should only be defined over recursively defined datatpes, described above. E.g. in CASL

is translated into PVS as follows:

reduce_nat, of type [nat,[nnatà nat]à [nnatà nat], is a function produced by PVS in the nnat_adt.pvs file created by PVS when nnat.pvs is typechecked. As is seen in the example, it gives a function from the datatype concerned to the built-in type of natural numbers (not to be confused in the example with the generated type nnat) which can then be used for generating measures. The term ‘reduce_nat (0,LAMBDA (x1:nnat):x1+1)(x1)’ is generated and stored by the translation when the nnat datatype is translated, so when any recursive function is translated the appropriate measure is generated by adding together the measures associated with each datatype in the arguments of the function. This will no doubt prove clumsy in specifications with many recursive datatypes and recursive functions defined on them and an obvious improvement is to declare e.g. a ‘stackmeas’ function with the datatype, to be used for any measure requiring it.

When typechecked the above example produces two type-correctness conditions, one to check that the accessor ‘pre’ is being applied correctly and one to ensure that the measure guarantees termination. They are as follows:

i.e. if n is not zero it must have been produced by the second constructor, suc,

i.e. that the measure strictly decreases for every step of the recursion.

The measure produced in translation will work for most simple examples but there are occasions when a more complicated measure will be required. E.g. the ackerman function on natural numbers, which can be written in CASL as

is translated to PVS as

and this produces (amongst others) the following type-correctness condition:

which is not true.

In such cases the user must supply an appropriate measure himself.

A CASL binary operation may be declared to have any of four ‘attributes’, associativity, commutativity, idempotency or possession of an identity element, and in translation to PVS these are explicitly written out as axioms. E.g. in CASL:

will be translated in PVS as:

Predicates are translated into functions onto PVS’s built-in boolean type. If they are recursive they need to be declared with the keword ‘INDUCTIVE’, e.g. on stacks

translates to

When this is typechecked PVS automatically produces a pair of implicit induction principles to assist in proving theorems about it. These are as follows:

In testing for recursion of operations or inductions I only test for recurrence of the identifier in the definition. So here overloading is not supported.

In addition basic items can declare variables or axioms. CASL can declare local variable axioms, in which the declared variables are local to specific axioms. This is semantically equivalent to universally quantifying these variables for each individual axiom and this is what happens in translation.

The first order logic of CASL is directly translatable into PVS with certain exceptions. CASL has existential equality and strong equality to deal with partial functions, but when all functions are total, these notions of equality are identical, so no distinction is made in the translation. CASL includes a ‘membership’ predicate asserting that a term belongs to some sort. This proved clumsy to translate to PVS and has been excluded. CASL includes an ‘exists uniquely’ quantifier, which PVS doesn’t. So it must be written out in full using a lambda term to affect substitution. E.g. a CASL formula

where the formula F contains x, is translated into PVS as:

CASL sorted terms, in which an expression is given with its sort, are fully translatable into PVS as coercion expressions.

There are as yet no constructs for declaring theorems in CASL. The ad-hoc solution to this that was constructed was to declare theorems in CASL as axioms starting ‘forall f:THEOREM . F’ for a formula F. This is translated into PVS as a theorem declaration.

In PVS axioms and theorems require unique identifiers and these are supplied automatically.

Mixfix notation is not supported by PVS. So the translation of a mixfix identifier will omit the place-markers and run the tokens together. Invisible identifiers, consististing solely of invisible placeholders are not supported.

Chapter 5

When using tools to manipulate or store CASL specifications an intermediate form of representation for specifications is required to allow easy transfer of specifications between the tools and it has been agreed [BKO98] to use the Annotated Term Format or ATerm. The ATerm datatype was developed as a means of exchanging and storing complex, possibly tree-like data structures such as syntax trees in a way that is software independent, easy to use and efficient [BJKO99]. ATerms may be transferred or stored in an efficient ‘Binary ATerm Format’ or as a human-readable text file or string. A library of functions for creating and manipulating ATerms has been implemented in C and Java1.2 and the Java ATerm Library was chosen for this project because of Java’s ease of use.

It was decided to make use of the HOL-CASL parser, developed by the Bremen CoFI group for their HOL-CASL project to embed CASL in the theorem prover Isabelle [MKKB98]. This performs parsing and static semantic checking on concrete CASL specifications, converting them into an abstract syntax tree in ATerm format based on an adapted version of the abbreviated abstract syntax of CASL in [CoFI98]. It also produces a global environment, listing the sorts, operations and predicates declared in a specification.

My implementation operates on the ATerm syntax tree to produce a file containing a PVS theory and further files for every datatype.

The Bremen Parser only deals with structured specifications. So the implementation first takes a ‘specification definition’ consisting of a name followed by a basic specification (but no genericity, as the program does not deal with parameterised specifications) and converts it into a PVS theory of the same name.

So given a CASL named specification as follows, saved as ‘example.casl’:

the parser will convert this to a textfile named ‘example.aterm’ and when my program is run it will take this file and produce three new files, ‘example.pvs’ for the main specification along with ‘nnat.pvs’ and ‘llist.pvs’ for the datatypes. example.pvs looks as follows:

And nnat.pvs and llist.pvs are as follows

When PVS is started and all these files are typechecked seven type-correctness conditions are generated, of which two are subsumed immediately and the other five are simple enough to be discharged automatically, and the theories nnat_adt and llist_adt are generated. After doing this the PVS prover may be invoked to prove the theorems.

The object of this project was to write a tool which translated CASL specifications into PVS. What I have achieved is a program which handles most of the constructs in CASL basic specifications while restricting attention to specifications with only total functions and a simple subsort relation, as described in the report.

Possible further work would involve expanding the implementation to deal with more CASL constructs and/or loosening the restrictions.

The main basic construct I did not manage to deal with is the sort generation constraint, which takes a collection of signature items and determines sentences declaring that the sort items declared are generated by the operations declared (with the exception of datatype selectors). This is the most difficult basic construct to handle because it requires the ATerm tree to be analysed to a greater depth than the other constructs and the pressure of time did not allow me to attempt this.

The constructs of structured CASL specifications are mainly concerned with combining basic specifications, adding elements, hiding elements forming a union of specifications etc, and achieving this would involve making use of PVS’s ‘IMPORTING’ construct, which allows PVS theories to be combined, with data hiding if desired.

The restriction on partial functions could be loosened in one of two different ways. Given a partial function f with domain D and range R it can be made total either by considering f to be total over a subtype of D or by adding an extra element to R to denote ‘undefined’.

Finally, the restriction on the subsorting relation might be relaxed if for each CASL subsort declaration the translation explicitly declared an embedding function from the subsort to the supersort, instead of using PVS’s subtypes.

I include here a listing, in full, of stack_adt.pvs, automatically generated by PVS when stack.pvs, described in Chapter 3, is typechecked.