7. Formal Specifications

SpecL object and operation definitions can be augmented with formal mathematical specifications. These formal specifications are in three forms: equational, predicative, and axiomatic. Equational specifications are defined by associating a set of equations with an object. Predicative specifications are defined by associating preconditions and postconditions with an operation. Axiomatic specifications are defined by associating a set of global conditions with all of the objects and operations within a module.

The predominant form of logical expression used in a formal specification is the predicate. Semantically, a predicate is a mathematical formula with a boolean (i.e., true/false) value. A predicate is fundamentally the same form of boolean expression as found in programming languages. However, predicates in SpecL can contain quantifiers and list operators that are typically unavailable in programming languages. In addition to boolean-valued expressions, SpecL provides numeric, string, and list-valued expressions.

This section of the report is a terse syntactic description of the elements of a formal specification. Section 8 to follow contains a tutorial discussion of formal specification, with examples.

7.1. Variable names

The base elements in an expression are variable names. Variables are declared in name/type pairs that appear in component expressions, input/output lists, and other contexts. Syntactically, a variable name is an identifier.

The reader should note the distinction between a variable name, used in an expression, versus an object name. An object name is defined using a complete object definition. That is, object names are those and only those names defined in definitions starting "object object-name ... ;". In contrast, a variable name is defined only in the context of a name/type pair. Variable names are those and only those names defined as variable-name:object-name. Such name/type pairs appear in one of four syntactic contexts:

  1. composition expressions appearing in the components part of an object definition
  2. input/output lists in an operation definition
  3. equation variable definitions
  4. forall and exists clauses
The first two of these contexts were described in earlier in Section 3.5. The last two contexts are described shortly.

7.2. Functional, Arithmetic, and Boolean Expressions

A functional expression is the invocation of an operation or auxiliary function (auxiliary functions are defined below). The general form of a functional expression is: 

name(args,...)
where name is the name of a defined operation or auxiliary function and args are input arguments. Any defined operation or auxiliary function can be used in a functional expression. The argument types of functional expressions are type checked in the same manner that function calls are type checked in a programming language. That is, the number and type of arguments must agree with the input/output declarations in the named operation.

The standard boolean operators and, or, and not are used in predicates. Note that and and or have overloaded meanings in SpecL. In the context of a composition expression, and and or denote composition primitives. In the context of a predicate, and and or denote boolean operators. These two overloadings have fundamentally different semantics.

Predicates can contain the relational operators =, != (not equal), <, >, <=, and >=. These are defined between expressions of the same type. For numeric and string types, the relational operators are defined to use the normal rules of numeric and lexical comparison. For composite types, relational operators are operate componentwise.

Predicate terms can include standard arithmetic operators. The operators are +, -, *, /, div, and mod. Note that since a predicate must have a boolean value, arithmetic expressions can only be used in predicates in the context of other logical operations, such as comparisons. For example, "a+b" is a legal expression but not a legal predicate. "(a+b) > 10" is a legal predicate.

Finally, there is a specialized form of equality operator for tuples, that compares two tuple values for equality, except for selected components that differ. The operator is denoted

tuple-variable ~= tuple-expression except (exception and ... and exception)
where each exception is an equality expression of the form
tuple-variable. ... = ...
(See Section 7.4 for a discussion of tuple selector operations.) The expression can be read "tuple1 almost equals tuple2, except ... ". For example, suppose an object Triple is defined as 
object Triple is i:integer and s:string and b:boolean
and variables t1 and t2 are of type Triple. The expression 
t1 ~= t2 except (t1.i = t2.i + 1)
evaluates to true if t1 and t2 are equal, except for the component t1.i, which has the value of t2 + 1. This "almost equal" operator is primarily useful in operation postconditions, where the value of an output tuple differs in only one or a few components from the value of an input tuple of the same type. Section 7.8 covers preconditions and postconditions in detail.

7.3. List Operations

List operations available for use in predicates are: + (concatenation), - (deletion), the list selection operation described in the next subsection.

List concatenation can be used on operands of the same list type, or on one list operand and one operand that is the base type of the list operand. List deletion requires the first operand to be a list and the second to be the base type of the first.

As noted earlier, a list has the structure of an ordered bag. With respect to the list operations, this means that list concatenation adds a new copy of the same element each time it is used. Complementarily, list deletion deletes one copy of an element in a list, if at least one exists. The list membership operator returns true if one or more copies of an element are present in a list. Given these semantics, the list cannot be used directly to model the structure of a set-like object. Rather, equations or predicates need to be used to define a set-like structure. Examples of such formal definitions are given later in the manual.

7.4. Composite Object Selector Operations

When an object is declared with multiple anded subcomponents, there is a built-in and selector operation for each such component, as the following general definition illustrates: 

object Foo is
   components: foo1:Foo1 and foo2:Foo2 and ... and foon:Foon;

   (*Built-in operations:*)
        SelectFoo1: (Foo) -> (Foo1);
        SelectFoo2: (Foo) -> (Foo2);
                . . .
        SelectFoon: (Foo) -> (Foon);
end Foo;
An alternate, ``syntactically sugared'' notation for and-selector operations is the infix "." operator Using infix ".", the following two terms are the same: 
SelectFoo1(foo)  is equivalent to  foo.foo1
Note that the "." operation is analogous to the use of "." in a programming language. Namely, "." selects an and-component in the same manner that "." selects a record field in a programming language.

When an object is declared with multiple or'd subcomponents, there exist two or-selector operations for each such component, as the following general definition illustrates: 

object Foo
   components: foo1:Foo1 or foo2:Foo2 or ... or fooln:Foon

   (* assumable operations: *)
        IsFoo1: (Foo) -> (bool);
        IsFoo2: (Foo) -> (bool);
                . . .
        IsFoon: (Foo) -> (bool);
        SelectFoo1: (Foo) -> (Foo1);
        SelectFoo2: (Foo) -> (Foo2);
                . . .
        SelectFoon: (Foo) -> (Foon);
end Foo;
The operations prefixed with "Is" are used to determine which alternative a subobject is. The operations prefixed with "Select" are used in the same fashion as the selectors for an and-composed object.

An alternate, "syntactically sugared" notation for or-selector operations is the infix "?." operator. Using infix "?.", the following two terms are the same: 

IsFoo1(foo)  is equivalent to  foo?.foo1
An illustrative use of the or-selector is with an object that contains an error alternative. Consider the following example: 
object ValueOrError is
    components: val:Value or err:Error;
end ValueOrError;
If v is a variable of type ValueOrError, then v?.val is true if the component of v is of type Value; v?.err is true if the component is of type Error.

Per the definition of or composition, a variable of an or'd type can only contain one of its alternative values at any given time. The "?." operator provides the means to check which type an or'd variable currently contains, thus allowing components to be properly accessed. Hence, before accessing an or object via ".", it should be checked with "?" to determine if the desired component is the current value. If the "." selection operator is used to access a component that is not current, then the value of nil is returned.

When an object is declared with a list of subcomponents, there is a built-in list selector operation for an individual subcomponent and a sublist operation that selects a range of subcomponents. The following general definition illustrates these list selectors: 

object Foo is
    components: Foo1*;
    (*Built-in operations:*)
        SelectNthFoo1: (Foo,number) -> (Foo1);
        SelectMthruNthFoo: (Foo,number,number) -> (Foo);
An alternate, ``syntactically sugared'' notation for list-selector uses "[" and "]" brackets. Using brackets, the following two terms are the same: 
SelectNthFoo1(foo,n)  is equivalent to  foo[n]
as are the following two: 
SelectMthruNthFoo(foo,m,n)  is equivalent to  foo[m:n]
Note that the "[...]" selector operation is analogous to the use of "[...]" in a programming language. Namely, "O[n]" selects the nth component of a list- composed object in the same way that "A[n]" selects the nth component of an array in a programming language.

In relation to other predicate operators, ".", "?", and "[...]" have the highest precedence.

SpecL provides two operators to cast variables of a parent type into a child type that inherits from the parent. For example, suppose x is a variable of type P, where P is a parent class. Suppose further that type T inherits from P. The operators that cast x into the child type T are the following:

Operator Meaning
x?<T Return true if the value of x is of type T. This expression is in error if T does not inherit from P.
x.<T Select the value of type T from the variable x. The value of this expression is nil if the current value of x is not of type T, i.e., if x?T is false. This expression is in error if T does not inherit from P.

These two operators are natural extensions of the '?' and '.' operators for unions. I.e., the '?' operator for a union tests for one of its alternative types; similarly, the '?<' operator for a class tests for one of its alternative subclass types. The '.' operator for a union selects one of its alternative types; similarly, the '.<' operator for a class selects one of its subclass alternatives.

The following example illustrates correct and incorrect uses of these class operators. Incorrect usages are followed by a comment starting with "ERROR". Correct uses are followed by a comment starting with "OK". 

object GenericObj = gd:GenericData;

object SpecificObj1 extends GenericObj = ss1:SpecificData1;
object SpecificObj2  extends GenericObj = ss2:SpecificData2;
object SpecificObj1a extends SpecificObj1 = ss1a:SpecificData1;

object GenericData = integer;
object SpecificData1 = integer;
object SpecificData2 = integer;
object SpecificData1a = integer;

operation Test(go:GenericObj, so1:SpecificObj1, so2:SpecificObj2,
        so1a:SpecificObj1a) -> (boolean) =
(
    (*
     * The next three expressions show that the variable go of type GenericObj
     * is not directly compatible with variables of its subclass types.  In
     * order to obtain a value of a subclass type from go, the ?< and .<
     * operators can be used, as shown below.
     *)
    (go = so1)      (* ERROR: GenericObj is not type equiv to SpecificObj1 *)
        or
    (go = so2)      (* ERROR: GenericObj is not type equiv to SpecificObj2 *)
        or
    (so1 = so1a)    (* ERROR: SpecificObj is not type equiv to SpecificObj1a *)
        or

    (*
     * The next four expressions show how to use the ?< and .< operators to
     * test and select subclasss values from variable go.
     *)
    (go?<SpecificObj1 = true)   (* OK: go?<SpecificObj1 returns true if the
                                       current value of go is of type
                                       SpecificObj1. *)
        or
    (go.<SpecificObj1 = so1)    (* OK: go<.SpecificObj1 selects the value of
                                       type SpecificObj1 from go. *)
        or
    (so1.<SpecificObj1a = so1a) (* OK: so1.<SpecificObj1a extracts the value of
                                       SpecificObj1a from so1. *)
        or
    (go.<SpecificObj1.<SpecificObj1a = so1a);   (* OK *)
);

7.5. Logical Implication

Logical implication operations are implies ("=>", elseless if-then), iff ("<=>"), and if- then-else. The implies and iff operators are binary boolean-valued operators with the standard predicate logic definitions, defined by the following truth tables:

p q p implies q
false false true
false true true
true false false
true true true

p q p iff q
false false true
false true false
true false false
true true true

Syntactically, the boolean operators "=>" and if-then have the same meaning as implies. Syntactically, the boolean operator "<=>" has the same meaning as iff. The if-then operator can also produce a non-boolean value, as described next.

if-then-else is a trinary expression operator, not a control construct as in a programming language. In the expression

if T then E1 else E2
T is a predicate, E1 and E2 are each expressions. The value of the if- then-else expression is E1 if T is true, or E2 if T is false. The type of E1 and E2 must be the same, but need not be boolean. The generalized truth table for if-then-else is the following:

p q r if p then q else r
false x y y
true x y x

When the then and else expressions are boolean-valued, the expression

if p then q else r
is logically equivalent to
p and q or not p and r

The meaning of elseless if-then as a binary operator warrants further discussion. As a boolean operator, binary if-then is equivalent to implies, with the truth table defined above. As a non-boolean operator, the binary expression

if p then x
is equivalent to
if p then x else nil.

7.6. Quantifiers

Universal and existential quantifiers can appear in predicates. In normal mathematical notation, universal quantification is represented by an upside down "A" and existential quantification by a backwards "E". In SpecL, the quantifier operators are forall and exists. The general form of universal quantification is

forall (x:t) predicate
read as "for all values x of type t, predicate is true" where x must appear somewhere in predicate. The general form of existential quantification in SpecL is
exists (x:t) predicate
read as "there exists an x of type t such that predicate is true", where x must appear somewhere in predicate.

In textbook predicate logic, universal quantification commonly takes one of the following two syntactic forms:


(1)  forall (x | p1(x)) p2(x)
(2)  forall (x in S) p(x)

The reading of form (1) is "for all values x such that predicate p1(x) is true, p2(x) is also true". The reading of form (2) is "for all elements x in set S, predicate p(x) is true"

In SpecL, the forall operator quantifies over all values of a particular object type. In comparison to forms (1) and (2) above, the general form of universal quantification in SpecL is 

forall (x: O) p(x)
The reading of this SpecL form of quantification is "for all values x of object type O, predicate p(x) is true". The reason that SpecL quantifies over object types is that SpecL is based on typed logic. This means that all variables that appear in SpecL predicates must be of some object type. In many mathematical treatments of quantification, the issue of strong value typing may not arise, and hence the notion of quantifying over types does not arise.

The fact that SpecL is based on typed logic does not restrict how universal quantification can be used, it just means that the use of universal quantification in SpecL must take typing into account. Therefore, the specific format of quantification is slightly different than in untyped logics.

Both quantification form (1) and form (2) above can be easily represented in SpecL. The SpecL for universal quantification form (1) is: 

forall (x:SomeObject) if p1(x) then p2(x)
where the predicates operations p1 and p2 take SomeObject as input and output boolean. The SpecL notation for universal quantification form (2) is: 
forall (x:Elem) if x in S then p(x)
where object S must be composed of Elem*. Since these two forms of quantification are quite typical, SpecL provides alternative syntactic notation to express them conveniently. Specifically the following two SpecL forms correspond to universal quantification forms (1) and (2) above:
(1) forall (x:t | predicate) predicate
(2) forall (x in list) predicate
In form (2), list must be a list-composed object, and x will be of the component type of list. For example, 
object SomeSet is
    components: Elem*;
    . . .
end SomeSet;

operation SomeSetOp is
    inputs: s:SomeSet;
    outputs: s':SomeSet;
    postcond: forall (e in S) f(e);
end SomeSetOp;
In this example, e is a variable of type Elem within the body of the forall.

Common extended forms for existential quantification are the following:


(1)  there exists (x | p1(x)) p2(x)
(2)  there exists (x in S) p(x)

The reading of form (1) is "there exists an x such that p1(x) and p2(x) is true". The reading of form (2) is "there exists an x in set S such that p(x) is true".

In SpecL, the exists operator quantifies over all values of a particular 

exists (x: O) p(x)
The reading of this SpecL form of quantification is "there exists a value x of type O such that p(x) is true". Both existential quantification form (1) and form (2) above can be easily represented in SpecL. The SpecL for form (1) is: 
exists (x:SomeObject) p1(x) and p2(x)
where the predicates operations p1 and p2 take SomeObject as input and output boolean. The SpecL notation for existential quantification form (2) is: 
exists (x:Elem) x in S and p(x)
where object S must be composed of Elem*. Since these two forms of existential quantification are quite typical, SpecL provides alternative syntactic notation to express them conveniently. Specifically the following two SpecL forms correspond to existential quantification forms (1) and (2) above:
(1) exists (x:t | predicate) predicate
(2) exists (x in list) predicate
In form (2), list must be a list-composed object, and x will be of the component type of list. Note carefully the precise logical meaning of the basic and extended quantification notations. Specifically, the following logical equivalences hold: 
(forall (x:t | p1) p2) <=> (forall (x:t) if p1 then p2)
(forall (x in s) p) <=> (forall (x:basetype(s)) if x in s then p)
(exists (x:t | p1) p2) <=> (exists (x:t) p1 and p2)
(exists (x in s) p) <=> (exists (x:basetype(s)) (p1 in s) and p2)
where basetype(s) is the type of components of which s is a list.

In the standard semantics of predicate logic, the value of a universal quantifier expression is true iff all instances of the quantified predicate are true. If one or more instances of the predicate are false, then the value of the entire quantifier expression is false. In the extended forms of universal quantification, it may be possible for the quantification expression to yield no instance values over which the quantifier applies. For example, consider the following quantification expression when the list l is empty: 

forall (x in l) p
With l an empty list, x assumes no values, and therefore predicate p is never evaluated. In such cases, the value of the entire quantifier expression is true. Close examination of the equivalent form of the extended quantifier expression confirms that a true result is sound in this case. The equivalent to the preceding list-based quantification is 
forall (x:B) if x in l then p
where B is the base type of the list l. In this form of the quantified expression, the quantified predicate always yields a value of true, since the subexpression x in l is always false, and by the definition of logical implication, "if false then x" is unconditionally true. Therefore the value of the entire quantifier expression is true.

Section 8 below contains further examples on the use of universal and existential quantification in SpecL.

7.7. Let Expressions

When the logic of an expression is complex, it can be useful to decompose it using let expressions.

The general form of a let expression is the following:

let name-list = expression
where name-list is a comma-separated list of variable names.

The purpose of a let expression is to define a name that can be used in place of the full expression on the right-hand side of the ``=''.

Let expressions are used within expression sequences of the following form:

( expression1 ; ... ; expressionn )
The value of such a sequence is the value of the last expression. Consider the following example: 
function T(a,b,c: boolean) -> boolean =
(
    let x = a and b or c;
    let y = a or b and c;
    let z = (a and b) or (c and b);

    if x
    then y
    else z;
);
In this example, the definition of function T is an expression sequence containing three let expressions, followed by an expression that uses the let variables. The value of the function is the value of the if-then-else expression, which is the last in the expression sequence.

It should be noted that the let expression does not have the same semantics as an assignment in an imperative programming language, such as Pascal or C. A let expression simply gives a name to an expression; it does not change the contents of some memory location. For those familiar with the C language, a let expression has the semantics as a #define macro definition.

7.8. Pre/Postconditions, Equations, and Axioms

Preconditions and postconditions are associated with an operation by including precondition and/or postcondition declarations within the operation definition. The syntactic forms are:

precondition: predicate ;
postcondition: predicate ;
where predicate is a legal SpecL predicate expression. Typically, conditions are made up of a number of predicates, composed with boolean "and's" and "or's". Section 8 has a number of examples that illustrate the use of pre/postconditions in SpecL.

Equations are associated with an object by including an equation declaration within the object definition. The general form of equation definition is the following:

equations:
var var_name:object_name, ... ;
functional_expr == quantifier_free_expression;
... ;
where a functional_expr is as defined above, and a quantifier_free_expression is an expression that contains no quantifiers or list operations. Note that the quantifier_free_expression is not limited to a boolean value, that is, it need not be only a predicate. The variable declaration(s) that precede the equations define auxiliary variables that are used in the equations. Section 8 contains example equation definitions in SpecL.

The "==" operator and the "=" operator should not be confused. The "==" separates the two sides of an equation; it has the lowest precedence of any infix operator. The "=" is the logical equality operator, which returns a boolean value. It has the same precedence as the other comparison operators.

Axioms are associated with all of the objects and operations defined within a module. Syntactically, an axiom is a predicate:

axiom: predicate ;

It is important to note that quanifying over a particular type T does not extend to any types that inherit from T. Consider the following example: 

object Parent = name:string and ...
object Child extends Parent = ...;
axiom forall (p:Parent) p.name != nil;
The stated axiom applies to all values of type Parent, but not to values of type Child.

7.9. Auxiliary Functions

As noted in Section 1.3, the objects and operations in an SpecL specification should be those that are visible to end-users of the specified system. When a specification is fully formalized, it is sometimes necessary or convenient to define auxiliary functions that are referenced in pre/postconditions or equations. An auxiliary function differs from an operation in that it is not intended to be visible to the end user of the specified system.

Consider the following example: 

object NumericPair is
    components: n1:Number, n2:Number;
end NumericPair;

operation DoSomethingWithPairs is
    inputs: p1: NumericPair, p2: NumericPair, s: SomeOtherObject;
    output: s':SomeOtherObject;
    precondition: if PairwiseLess(p1,p2) then ... ;
end DoSomethingWithPairs;

function PairwiseLess(p1:NumericPair, p2:NumericPair) : (boolean) =
    (p1.n1 < p2.n1) and (p1.n2 < p2.n2);
Here the auxiliary function PairwiseLess is defined. This function takes inputs p1 and p2, both of type NumericPair. It produces a boolean output. The following is the general format of an auxiliary function:
function name (list of inputs) : (list of outputs) =
body
end name
The function body is an expression of the output type(s). If the function produces a single output, then the body is an expression of that type. If the function produces more than one value, then the body is a list of expressions enclosed in square brackets, where each expression corresponds ordinally by type to each of the output parameters.

While PairwiseLess is not strictly necessary in the preceding example, it can make the specification clearer and more concise, particularly if PairwiseLess is used in several different preconditions and postconditions. The next section contains further examples on the use of auxiliary functions and a discussion of when their use is appropriate.



Prev: user-attrs | Next: formal-spec-examples | Up: index | Top: index