From: jcm@hgc.edu (James McKim)
Subject: Re: Assertions for programming design
Organization: The Hartford Graduate Center
Date: Mon, 6 Apr 1992 14:31:03 GMT

In article <1992Apr3.104752.17417@sun.pcl.ac.uk> priestm@sun.pcl.ac.uk (Mark Priestley) writes:
>In article <1992Apr1.143335.27588@merlin.hgc.edu> jcm@hgc.edu (James McKim) writes:

[Discussion of earlier stack "specification" deleted]

>>  What have we gained? Well, let's see...
>>  We know that depth is callable anytime. We know that depth changes
>>  on Create, push, and pop. We know exactly how depth changes in each
>>  case. We know that push is callable anytime, but that pop and top
>>  are callable only when depth > 0. We know that top changes after
>>  push and pop. We know exactly how top changes after a push. All of the
>>  above can be automatically checked or enforced. The _only_ part
>>  that is not rigorously specified is the value of top after pop.
>
>Very true. There seems to be a conflict in this example between the desire to
>use assertions as specifications and the desire to generate run-time checks
>from assertions. To do the latter you need a simple Boolean expression that can
>be evaluated at a single fixed point in the code, eg at the end of a routine,
>but this is not a sufficiently powerful mechanism to specify the interaction
>between two routines, as in this case.

Well said!
 
>
>One way of doing it would be to add "class axioms" to the language, by analogy
>with the "package axioms" used in Anna (an annotation language defined by David
>Luckham et al for specifying Ada programs: described in a book "Programming
>with Specifications", pub. Springer Verlag). This would allow the writing of
>assertions like (excuse the syntax which I've just made up)
>
>    after (push;pop) : top = (old self).top
>
>- but it would take a *lot* of work to translate this into run-time checks.

Is the translation into run-time checks done in Anna? Enquiring minds... :-)

>
>The other possibility is to use an auxiliary routine, like "item" - but then
>there is the problem of specifying that "nothing else changes". For example,
>given the specification
>
>>  push( x : T )  is 
>>  ensure
>>    depth = old depth + 1 ;
>>    item( depth ) = x ; 
>>  end ; -- push
>
>there is nothing to prevent an implementation of push from altering every value
>returned by item for values different from depth.
>

Well, there are only a finite number of attributes in a class, so I'm
not convinced there is any theoretical problem with specifying  "nothing else 
changes". There may well _be_ such a problem and I just don't see it yet.
Certainly there is no such problem in this example. Making up some syntax
of my own, we just need something like

  for_all i, 1..(depth-1) (item(i) = old item(i))

as a postcondition on both push and pop. Obviously life for the
designer of the class would be a lot simpler if "no change" is the
default. 

>(BTW, these two strategies seem analogous to the axiomatic v. model-based
>divide in specification languages: the use of class axioms is ..er.. axiomatic
>specification, whereas the use of an auxiliary routine like "item" is an
>attempt to construct a model of what a stack is - eg it's a bit like a
>sequence, in this case.)

Yup, again nicely put.

>
>> >Sounds pretty close to a full specification to me. :-) >
>
>On the other hand, if a plane crashes on landing, you're not pretty close to a
>successful flight :-)

Cute, but a bit of a non sequitur. At least I _hope_ you're not saying
that a partial specification is no better than none at all. To me,
_specifying_ nothing because we can't specify everything makes as much
sense as _testing_ nothing because we can't test everything.

>-- 
>Mark Priestley  (priestm@sun.pcl.ac.uk)
>School of Computer Science ...
>Polytechnic of Central London


Regards,
-- Jim
-- 

*------------------------------------------------------------------------------*
Jim McKim  (203)-548-2458     In exactly 3.2 seconds it will be a few 
Internet:  jcm@mstr.hgc.edu   minutes to 5:00.
Newsgroups: comp.lang.eiffel