Introduction to Data Structures

			 ASSERTION NOTATION

			   Gary T. Leavens
	Department of Computer Science, Iowa State University
		      Ames, Iowa 50011-1040 USA
			leavens@cs.iastate.edu
		     $Date: 1995/03/23 08:16:10 $


			       Abstract

A summary of the differences in notation for informal specifications
used versus Appendix D of Headington and Riley's book
``Data Abstraction and Structures'' (D.C. Heath, 1994).


0. OVERVIEW

See section 1.6 of Headington and Riley's book for an introduction to
this topic, and then read their appendix D.

The differences described below apply to program examples discussed in class,
and should be followed on homeworks.  However, they do not apply to examples
in Headington and Riley's book, which was printed before these were written.


1. INTRODUCTION

Like Headington and Riley, in Com S 228, we use logical (Boolean) statements
in English to specify the states of computations at specific locations within
a program.


2. TYPES OF ASSERTIONS

We use the same types of assertions as Headington and Riley
(ASSERT, INV, PRE, POST, and CLASSINV).  The differences are only in
the usage of loop invariants and class invariants.

However, we also use a MODIFIES clause, which summarizes information
about the post-condition (POST).  Because of this do not use the annotations
	/* in */, /* out */, and /* inout */
on function parameters.

Finally, we also add a LET comment, which allows binding names to values,
for use in assertions later in the code.

2.1 INV (loop invariants)

A loop invariant describes a relationship between variables that is
unchanged by the execution of the loop's body.

For a loop whose test has no side effects, the loop invariant should
hold in three places: before the loop, just after the test,
and at the end of the body.  For example, here is a loop that commputes
the factorial of n.

	// ASSERT: n >= 0
	fact = 1;
	i = 1;
        // ASSERT: fact == (i-1)! && i <= n+1       *
	while (i <= n) {
          // ASSERT: fact == (i-1)! && i <= n+1     *
	  fact = fact * i;
	  i++;
          // ASSERT: fact == (i-1)! && i <= n+1     *
	}
        // ASSERT: i > n && fact == (i-1)! && i <= n+1
	/* hence */
	// ASSERT: fact == n!

The three starred assertions are the loop invariant.
It is a considerable notational convenience to only write such an invariant
once.  Headington and Riley commonly write "INV (prior to test)",
meaning that the invariant is to hold before the test,
but write the invariant inside the loop body.

	// ASSERT: n >= 0
	fact = 1;
	i = 1;
	while (i <= n) {
          // INV (prior to test): fact == (i-1)! && i <= n+1
	  fact = fact * i;
	  i++;
	}
        // ASSERT: i > n && fact == (i-1)! && i <= n+1
	/* hence */
	// ASSERT: fact == n!

We will accept this notation, but in our own programs will write the
code like the following, with the understanding that it means that the
invariant has to hold prior to each execution of the test.

	// ASSERT: n >= 0
	fact = 1;
	i = 1;
        // INV: fact == (i-1)! && i <= n+1
	while (i <= n) {
	  fact = fact * i;
	  i++;
	}
        // ASSERT: i > n && fact == (i-1)! && i <= n+1
	/* hence */
	// ASSERT: fact == n!


2.2 CLASSINV (class invariants)

Headington and Riley say that it is the user's responsibility
to ensure that the class invariant is true before invoking a class operation.
In our specifications, the class invariant can be assumed to be true
before invoking such operations (except constructors).

2.3 MODIFIES CLAUSE

The modifies clause lists variables (objects) that can be changed in any call
where the precondition (PRE) is satisfied.  They don't have to be changed,
but no other variables (objects) can be changed.
For example, we would specify Discount, at the top of p.116 as follows:

	void Discount(float & cost, float discountRate)
	  // PRE: true
	  // MODIFIES: cost
	  // POST: cost == cost<entry> * (1.0 - discountRate)

This means that a call to Discount cannot modify anything except cost
(that is, it cannot modify anything except what cost refers to during the
call).  You can read it as "modifies at most" when pronouncing it.

Note that the streams cin, cout, and cerr are considered variables,
and so should be listed in a function specification if that function
can do input or output.  For example, the following is a specification
of a function that prompts on cout.

	extern void prompt(char *promptstring);
	  // MODIFIES: cout
	  // POST: promptstring has been added to cout, and cout is flushed.

An omitted MODIFIES clause means
	// MODIFIES: nothing
by default; we take this to mean that no variables can be modified.

Because we use the MODIFIES clause, we do not use the annotations
	/* in */, /* out */, and /* inout */
on function parameters.  We also do not use the Assigned notation, see below.


2.4 LET ASSERTIONS

Sometimes it is useful to have names for values of variables that are
being changed in a function.  This is the purpose of a LET assertion.
For example.

	double fact(unsigned int n)
	  // POST: FCTVAL is n! (the factorial of n)
	{
	  // LET oldN = n
	  double f = 1.0;
          // INV: f * n! = oldN! 
	  while (!(n == 0)) {
	     f = n * f;
	     n = n-1;
	  }
	  // ASSERT: n = 0 and f * n! = oldN!
	  return(f);
	}

One could, of course, use C++ variables for such purposes.  For example,
one could declare the name oldN as a unsigned int variable (or constant)
above.  However, that introduces a cost in both space and possibly time.


3. NOTATION WITHIN ASSERTIONS

We use the notation of Headington and Riley with the following exceptions.

3.1 Assigned(X) 

We do not use this assertion, because it is not testable.
See Section 2.3 above for an example.


4. FORMATTING DIFFERENCES

We often omit the comments of the form
	//--------------------------------
and
	//.................................
which Headington and Riley use to set off their abstract and concrete
specifications in code.

We also permit comments to be given in C style.  For example, one
can format specifications as follows.

	void Discount(float & cost, float discountRate)
	  /*
	   ** MODIFIES: cost
	   ** POST: cost == cost<entry> * (1.0 - discountRate)
	   */


5. OTHER COMMENTS

In the specification of a C++ class, we use a comment of the form

	// ABSTRACTLY: mathematical rationals

or Headington and Riley's form of this comment

        // DOMAIN: mathematical rationals

to describe the abstract values and the vocabularly to be used in the
class invariant, and in pre and postconditions of member functions.

In the .pri file for a class we use a comment of the form
        // ABSTRACTION MAP: ...
to say how the data members implement the abstraction.

For example, for the type account there is in the file Account.h the 
comment:
           
	  // ABSTRACTLY: a balance in dollars

and in the file Account.pri the text.
	private:
	  int numCents;
	  // ABSTRACTION MAP: self's dollar balance is numCents / 100.


ACKNOWLEDGEMENTS

Al Baker has helped develop these conventions (although his are slightly
different in minor details).  The idea of the MODIFIES clause goes back
is adapted from Jeannette Wing's Larch/CLU interface specification language.
The idea of specification using abstract values goes back to C.A.R. Hoare.