Conference turris::languages

I think a post-condition is supposed to help prove that
the function does what it is supposed to do.  But proving that
(FOO=TRUE or FOO=FALSE) when the function is done, will not add
anything towards proving the correctness of your program!

I doubt any serious real world usages of program verification
exist so far, precisely for the reason you are encountering -- it
is not at all obvious how to use concepts like pre and post
conditions as soon as things get a little complicated.

However, ASSERT is widely used in C and C++ programming.  I
don't know about whether similar constructs are being used in
other languages, but I suspect they are.

  /Mukesh

    By the way, the Ada 9X formatting standard is going to look like this
    
    
    	function Search(X : Integer_Array; Key : Integer) return Integer;
    
    
    which I think most people will agree is a lot neater than the Ada 83
    
    
    	function SEARCH(X : INTEGER_ARRAY; KEY : INTEGER) return INTEGER;
    
    
    although both of these look nicer than the non-standard
    
    
        FUNCTION search(X:    IN integer_array
                       ;KEY:  IN integer)
                 RETURN integer;
    
    
    style that you are showing here.
         
    
    /Bevin

    Re .1
    
    I'm not sure what counts as a real-world application but I thing that
    someone over here in the UK has produced / is producing a Z formal
    specification for the OpenVMS distributed lock manager...
    
    	Rik
    
    PS The last time I looked the (not yet completed) formal semantics for
    Ada-83 was over a meter long and growing.

    .3
    
    hi,
    
    but what's the point of making formal specifications for something
    allready been written and completed long ago (the distributed lock
    manager) ?
    
    i must be missing something here.  
    
    \nasser

    \nasser
    
>    but what's the point of making formal specifications for something
>    allready been written and completed long ago (the distributed lock
>    manager) ?
    
    If you *can't* do it then something must be wrong. So, being able to
    complete the spec increases confidence in the code (more likely it will
    reveal some bugs that noone noticed before ;-). Either way, a worthwhile
    exercise.
    						John Gillings, Sydney CSC
    

re .1

>    FUNCTION foo(input_line: IN string; io_file : IN FILE)
>
>    pre: string'length != 0 and io_file'status = OPEN
>
>    post: string'length !=0 
>          AND io_file'status = OPEN 
>          AND  (foo=TRUE or foo=FALSE)

You don't have to repeat the 'pre' in the 'post', .2 is right, the post
function tells you not only what values can be passed back (what you did), but
also why. Translated to your question in .0:

 pre: string'length != 0 and io_file'status = OPEN

 post: foo=TRUE when foo_1 ends with success
       foo=FALSE when foo_1 ends with an error        

Talking about the successfull write to the file and the parse is done in the
post condition of foo_1.
post condition does not have the lines "string'length !=0" and "AND
io_file'status = OPEN" repeated because if post does not mention something,
it's not changed.

Bert Catsburg
    

        .6
>       post: foo=TRUE when foo_1 ends with success
>       foo=FALSE when foo_1 ends with an error        

    but this is NOT a predicate !
           
    the DEFINITION of a pre and post condition is that it evaluates to TRUE
    or to FALSE.

    also the book definition of pre and post is that they apply over all the
    parameters, they make a statement about the parameters at the end of the
    function that must evaluate to TRUE or FALSE. in your's above the post
    did not address the state of the the string length and the io_file
    state.

    iam starting to think this pre and post condition is all hack wash.
    
    untill i see a real world software project spec'ed this way, i'll
    just learn this to pass the exam and nothing more.
    
    Z and VDM however have been used in real world spec's, but i know
    little about these other than looking at simple examples using them,
    they are more complex and need time to learn.
    
    \nasser

You may also receive more expert response in the FORMAL_METHODS conference at 
COOKIE::FORMAL_METHODS

Peter.

  RE: .3,.4,.5

	I am the author of the lock manager specification alluded to in .3. It
was written as part of the requirements for an M.Sc in Computation, primarily
to teach me Z and CSP. (It succeeded.)

	As .5 points out, back-fitting formal specifications to existing
software can have benefits and IBM have done this quite extensively with CICS
(they halved their customer reported fault rate.)

	For what its worth, what Nasser (\nasser ?) is talking about is not
formal specification but code annotation. To get the real benefits you have to
use the pre and post conditions together with a collection of re-write rules
often referred to as the "Laws of Programming". A good introduction to this is
a book by Carroll Morgan called "Programming from Specifications". Based on my
experience doing an M.Sc, this is not the sort of thing any normal person is
likely to learn by just playing about. It takes some fairly intensive study.
        
	If anyone is interested in this please feel free to contact me.

	Geoff Winn.

ref .-1
    
    thanks \Geoff for the info.
    
>likely to learn by just playing about. It takes some fairly intensive study.
    
    yes, one of the "disadvantages" of formal specs is that it does
    require this extensive trainign and study to learn it, and use it.
    
    one of its advntages is: (1) since it is formal, one can come up with
    a tool to verify the correctness of the specs, and (2) possibly
    even come with a tool to take the specs and generate the code .
    
    \bye
    \nasser

What I don't understand, and perhaps someone could clarify, is:

If a formal spec is formal enough to cross all t's and dot all
the i's, how is it different from what we call a "programming
language"?  And if it is vague and wishy-washy, what good
is it?

In other words, by the time you specify that "if the disk happens
to be full when you attemp this write operation, then the spec
requires that a message be printed out at the operator
console", it begins to sound like any programming language.

If you don't specify to this level of detail, what is there to
claim that anything proved by the formal specification can be
trusted, or that what is proven is of any real use to anybody?

If you just want to design a "very high level" programming
language, why not call it that?

This is not meant to be a put-down of formal methods and the
study thereof, since even if the goal were to be unreachable,
there still might be many side-effects which might result
from the field which could be put into practice to **improve** the
practice of coding.

But I am curious as to how the practicioners of the field
view it.

    A simple example of a formal spec which is good enough to write a
    program from but is definatly not a programming language would be
    something like this.
    
    In pseudo VDM :
    
    Function Sqrt Calculates the square root of it's argument. To an agreed
    ------------- precison (delta)
    
    
    	PRE	: x >= 0, delta >= 0.
    
    	POST	: -delta <= (result * result) - x <= delta.
    
    
    	Note that it doesn't tell you anything about how you calculate the
    result (the implementation) only what the result should be (the
    specification)
    
    	Rik -very-long-time-since-he-did-a-VDM-course-and-it-shows...

But I am still not sure I see the fundamental thrust.  (Btw, the
same response was posted by Win Treese but "reply" didn't work
so he just forwarded it in mail to me.  I am not posting it
since it is the same "sqrt" example.)

I see the advantage of re-specifying something a few different
ways, some of which can only be post conditions.  Since
this provides "cross checks".

Even if one didn't re-word the complete specification, one
could still write cross-checks, e.g. "at the end of this
function, foo should not be 0". That is advantageous too, and
these have already been appropriated by the programming
community as "Assert"s.

But what is to "prove" that the said re-wording is
correct?  Doesn't it just depend upon the ability
of the re-worder?  While I agree that such cross
checks would improve programming by reducing the
possibility of error, I don't see any provability.

Another way to write the spec in .12 would be:

POST:  result = sqrt(x)

Which is why I called the spec a "re-wording" of the
obvious way to specify.

        .14

    in pre and post "specifications" , or whatever you want to call it, 
    these conditions supposed to show to the reader what the boundaries
    of the input parameters are before you enter the function and at the
    end of the function also to show the boundaries (possible values, 
    limits, ranges etc..) of the parameters .

    for me, this is nothing more than formal documentation of the function
    one is to code. it is supposed to help show more clearly what will
    happen to the parameters values before and after.

    
    \nasser

Is it really possible or useful to be equally "formal"
with most problems as it is with simple mathematical ones?

If boundary conditions are the only useful results, note
that the example did not take into account overflow
and underflow, or hardware errors.  If you can hand-wave
these away, I think it is quite reasonable to hand-wave
away the boundary conditions for sqrt in any but the
most rigorous numerical-analysis oriented work.  And
for that kind of work where the boundaries of sqrt
are important, they *are* specified in the straightforward
wording as well.  In the example, we are formally specifying
boundary checks of little real use to anybody (some
kind of boundaries are implicit in the understanding
of "sqrt", as they are in understanding of "+", "-" etc.)

We could make this discussion more concrete with
a real formal and useful answer to your .0

	Well, this is more interest in Mathematics than I've seen in a long
time ...

	To answer .11 and .13 I think we need to go back a bit.

	What Nasser was originally talking about are usually called Hoare
Triples. In the general case we have

	{ P } S { Q }

where P and Q are predicates and S is a program. This should be read as - if P
is true, and we run the program S, it is guaranteed to terminate and when it
does, Q will be true. Being mathematical predicates, P and Q are unambiguous in
a way that most program documentation isn't ("Allocate some memory").
Furthermore, they are quite general predicates about the state of the system.
They are not confined to describing parameters.

	Now it happens that, given P and Q, there are laws of programming that
we can apply that will generate S for us. These laws provably retain the
relationship between P and Q. Therefore, when we complete the process of
obtaining S, we have a proof that this S really does achieve Q when started
from P. This is quite different to the conventional technique where I tell you
I want to get from P to Q, you go away and write some code and then come back
and assure me that it does what I want. You may even have tested it a couple of
times. This is the important use of proof. We start with a mathematical
specification (the P and Q) which describes _what_ is to be achieved. Then we
use the specification to derive code which _provably_ achieves what we want.

	Of course, none of this changes the fact that getting from P to Q may
be of no interest to anyone, but that's another question ...

	Geoff Winn.

	My previous reply was written before .16 appeared. I'll give that some
  thought over the weekend and see what I can do. One point to bear in mind is
  that its hard to find an example which is small enough and simple enough to
  discuss here and also be a solution to a worthwhile problem. Suppose I asked
  you to _show_ me that your favourite programming language can be used for
  large scale projects (dozens of developers and many hundreds of thousands of
  lines of code). In a notes entry this might be difficult. This is not to
  criticise your question. Just try to be reasonable about how much you expect
  to see via this medium. (For example, much of the mathematical notation
  cannot even be rendered this way.)

	Geoff.

Your message <[email protected]> was forwarded to
me for comment.

The short answer to your question is that every (fully-defined) programming
language IS an executable specification language, although perhaps not a
very perspicuous one.  And every executable specification language IS a
programming language, although perhaps not a very efficient one.

But not all specification languages are executable.  In fact, there are
good arguments for non-executable specification languages:

- They don't force you to make arbitrary choices about execution details
that you don't want to specify (e.g., the order in which the error tests
are done, or how elements with equal keys are ordered by a sort procedure);
i.e., they allow intentionally incomplete specifications, leaving more
freedom for the implementor to exploit in writing an efficient
implementation.

- They allow partial specifications to be combined with "AND".  This is
very powerful.  As far as I know, the only executable specification
languages that allow such a conjunction operator are those with
backtracking interpreters (e.g., Prolog).  But this is a very natural way
to compose specifications.  Consider a sorting procedure.  We would like
the output to have two properties:

  * The elements are in nondecreasing order

AND

  * The output is a permutation of the elements in the input.

It is not easy to combine a program that has just the first property with
one that has just the second to produce a program that has both.

When designing a specification language, clarity is the highest priority.
When designing a programming language, clarity is important, but may have
to be sacrificed in trade-offs with compilability, efficiency, etc.

For more on this topic, see "Some Notes on Putting Formal Specifications to
Productive Use," John Guttag, James Horning, and Jeannette Wing, Science of
Computer Programming 2, pp. 53-68, 1982, or the introductory material in
"Larch: Languages and Tools for Formal Specification," John V. Guttag,
James J. Horning, et al., Springer-Verlag Texts and Monographs in Computer
Science, 1993, ISBN 0-387-94006-5.

Jim H.

    Mukesh,
      Perhaps a little annecdote will help you see the important difference
    between these 2 types of language:
    
      My father once asked me to do a small job for him. He took a small
    cardboard box and led me out to the car. Pointing inside he said "Now
    you have to undo those 4 screws and pull that panel back. Behind it
    you'll find 4 wires attached to a circular plug..". "Hold on Dad, just
    what am I supposed to be doing here?" "I'm telling you aren't I? You
    undo those 4 screws and... (launching into the same stream)". While he
    was rattling on, I opened the box and found a new radio/cassette
    player. "Aha, I see now, you want me to install the radio!, OK, I can
    figure out how to do it myself thanks".
    
      He was using a "programming language" to tell me *HOW* to install the
    radio without telling me *WHAT* I was doing. I suppose I could have
    derived the *WHAT* part by listening long enough, but could I be
    certain that the *HOW* part actually implemented the correct
    specification? Given the correct specification, I didn't need the
    implementation details, they were self evident. 
    
      So, the specification tells us *WHAT* is to be done, deliberately
    leaving out the implementation details like which screws need undoing and 
    which panels need to be removed. On the other hand a programming
    language tells the machine *HOW* to do something. Some programs (very
    few ;-) make it clear from the text and comments *WHAT* they are doing,
    but it is actually not necessary - see the "obscure program" contests
    popular with C programmers (indeed, see *any* C program :-).
    
      This distinction between *WHAT* and *HOW* is extremely important and
    is ignored much too often. Many programmers cannot understand that
    programs are not just source code and cannot be written directly into
    a terminal. The hard work is understanding exactly what the program is
    supposed to do and designing (note, *NOT* coding) data structures and
    algorithms required to do it. Another short annecdote - a manager of
    mine once boasted to a colleague that one of his programmers (me) had
    produced a 7000 lines of working PASCAL code in a single day. It's
    certainly true that I typed it all in one day, what he failed to
    mention was that I spent about a month before hand, away from a terminal,
    working out the specifications and data structures. The easy part was
    translating them into code. One of the reasons I no longer write
    programs for my living is the difficulty in finding anyone who will
    allow me to work like that! They seem to want programs slapped together
    on the fly as quickly as possible, rather than programs that are
    correct.
    						John Gillings, Sydney CSC
                                                    

That's a good way to put it, John.  We also seem to have
developed another terminology for this as well: "high level"
vs "low level" languages.

In a high level language, one says "a = b * c", whereas in
the lower level language one may have to do things like
fetch, store...  In a very high level language, one might
say "do what I mean", or at least specify in everyday English!

Anyway, you do have a good point for developing formal specifications.
As .19 points out, these languages do not suffer from various
constraints which implementation languages have to acknowledge.

Incidentally, the belief that the program is being *proved* correct
is a mistake -- what is being proved is the equivalence of two methods of
specification.  This provides a good cross
check.  But the real specification starts off in the minds of
one or more people, at varying levels of clarity.  The translation
of this into formal details can be done using the so-called
formal languages, or the more traditional languages.  Neither
translation method is error proof.  Moreover, at least now, the
translation into formal methodology appears to be very complicated,
and therefore more error prone.  Note that a simple problem
such as that posed in .0 is too complicated to use for a
useful example.

I do agree in the long run the study of formal methodologies
is liable to give us useful results.  Even now, a cross
check is better than no cross check at all.  The more
cross checks, the less the chances of error: this is also
called "defensive programming".

  /Mukesh

PS  From your anecdote, you must be a very fast typist!!
I don't think many secretaries could type that much in a day.
Do you know your WPM?

       Two points:
    
    	- Formal methods give you a way to test when your implementation
    		is complete.  I.e. if you're implementing a state machine,
    		you can know you're done when you handle all the
    		possible states and transitions.
    
    	- Formal methods prove their worth when applied to well-bounded
    		problem areas.  For instance, proving that a locking
    		implementation is "correct" with respect to detecting
    		deadlocks, etc.
    
       Note that with both, the truly hard part, in my opinion, is getting
    to understand the desired implementation well enough to be able to
    fully specify the pre and post conditions to a transition.  For
    example, windowing user interfaces which usually try not to force the
    user into a specific pattern of response in order to deal with some
    collection of views of entities.  Given the current work in HCI, it's
    not just very difficult, but undesirable to construct a hard-and-fast
    model of correctness for a user-interface, because your implementation
    should always be open to adjustment based on user input.
    
       Basically, I personally think that formal methods are best applied
    to well defined and widely used software components, like an operating
    system or a threading package or a windowing system.  To attempt to use
    formal methods to ascertain the correctness of, for example, a GUI to
    an application, is very difficult, costly in terms of time and expense
    and is of questionable value given the desire to adapt UI designs as
    rapidly as possible to user input.
    
    					-mjg

  	I've been looking at Nasser's original question since a previous note
  suggested that it might be an interesting example. Unfortunately so far I
  only have more questions.

  from .0

  > according to this text, pre and post condition are a predicates over the
  > input and output of the function. a predicate is simply a boolean
  > expression which is true or false and whose variables are the parameters
  > of the function being specified.

	This is a very restrictive and unusual "definition". What text are you
  using?

  > the '' means the value of X array after the function has been evaluated,
  > although this is confusing since it seems to indicate X was modified,
  > which is not the case, any way, this is minor point).

	Well you have to have _some_ notation for before and after states or
  else you have no way to discuss them at all.

  > my question, is how to use the above per, post, predicates to spec
  > a function that does not modify its parameters and only return
  > a status, say TRUE or FALSE.

	I've tried to make sense of this example but I don't really understand
  what you are trying to achieve. As best I can tell foo is a trivial jacket
  to foo_1. Consequently, foo has a rather trivial specification. The
  interesting part is really foo_1. There really isn't a lot that you can say
  about foo.

  >  spec a function foo that take in an input line with size > 0 and
  >  pointer to a file (or simple a file say io_file) and then calls another 
  >  function foo_1 to parse the input line and foo_1 will also write the 
  >  parsed line to the file io_file that was already opened and then foo 
  >  will return the completion status form foo_1, whatever that was. status 
  >  can be only TRUE or FALSE

	So foo_1 has an interesting specification which does something with
  its input but foo does almost nothing. I think the real difficulty here is
  that foo does so little that the spec you generate looks "wrong". I think
  you should start with a spec for foo_1 and go from there.

>    FUNCTION foo(input_line: IN string; io_file : IN FILE)

>    pre: string'length != 0 and io_file'status = OPEN

>    post: string'length !=0 
>          AND io_file'status = OPEN 
>          AND  (foo=TRUE or foo=FALSE)

	I think you want a post condition that says that string and io_file
  are unchanged in the after state so probably

	string'' = string AND io_file'' = io_file
	AND (foo = TRUE or foo = FALSE)

>    i wish in these books they show more complicated and more examples
>    of using this kind of formal specs, most of the book I've seen use
>    this search example, all are very simple examples, and one or 2 of them
>    at the most.

	Try "The Elusive Software Refinery: a case study in program
  development", by Kenneth R Wood. (I've lost the rest of the reference but
  I'll mail him and get it.) I have a copy of this and it runs to about 30
  pages. It develops a three valued logic simulator using Z and the refinement
  calculus. It generates pseudo code at about the level of Pascal and was
  subsequently implemented in Occam. It also includes a lot of proofs. 

  from .1

  > I think a post-condition is supposed to help prove that
  > the function does what it is supposed to do.

	Not quite. The "proof" must show that the program achieves the post
  condition when started from a state satisfying the pre-condition. (When
  started from a state not satisfying the pre-condition it can do anything it
  wants.) As discussed in previous replies, the pre and post conditions
  specify _what_ must happen. The proof shows that the code really does do
  this. It is a _separate_ question as to whether the specification does what
  you (the customer) want. Essentially, if I build a food mixer and it never
  goes wrong and is clearly labelled as a food mixer and you buy it - it is
  not my fault if you find that it won't play your CDs.
          
  from .21

> fetch, store...  In a very high level language, one might
> say "do what I mean", or at least specify in everyday English!

	If this is what you mean by a high level language then it is not a
  formal specification. One of the main points about a formal spec is
  precision. "Everyday English" is certainly not precise.

> Incidentally, the belief that the program is being *proved* correct
> is a mistake -- what is being proved is the equivalence of two methods of
> specification.

	I don't think this is a mistake. It is one of the meanings of proof.
  Ie we seek to prove that one description of the problem (a formal
  specification) is "equivalent" to some other description (code). I'm not
  aware that any other meaning has been attributed to "proving a program
  correct".

  	A second use of proof (unrelated to proving program correctness) is
  probing the quality of the specification. Given a formal spec you can
  construct proofs of properties that _must_ follow from the specification
  even though they are not explicitly stated. For example, in specifying an
  editor you might specify operations to insert and delete a character. You
  would probably expect that an insert followed by a delete would leave the
  document unchanged. If you _can't_ prove this from your spec then you have a
  strong hint that something is wrong.

  > But the real specification starts off in the minds of one or more people,
  > at varying levels of clarity.  The translation of this into formal details
  > can be done using the so-called formal languages, or the more traditional
  > languages. Neither translation method is error proof. 

	Ok with me so far but ...

  > Moreover, at least
  > now, the translation into formal methodology appears to be very
  > complicated, and therefore more error prone.

	Now this is just plain wrong. If you go from the "real specification
  in someone's mind" to "more traditional languages" then you sat down with a
  piece of paper (or worse, at a terminal) and wrote code. You can't tell me
  this isn't _strongly_ "error prone". By contrast, writing a real formal spec
  demands considerable care and forethought and pretty much forces you to
  understand what you are doing. Even if you then go away and write the code
  by hand (ie the "formal" spec is being treated as just a different way of
  writing a functional spec) you _still_ have a much better understanding of
  what you are doing.

  > Note that a simple problem such as that posed in .0 is too complicated
  > to use for a useful example.

  	And this is wrong too. It isn't too complicated. It just isn't clear
  (to me) what is wanted. It may in fact be too simple.

  	Geoff.

	The paper I referred to in .23 is

  The Elusive Software Refinery:  A case study in program development by
  Kenneth R. Wood in [Proceedings of the] 4th Refinement Workshop, edited by
  Joseph M. Morris and Roger C. Shaw, published by Springer-Verlag in the BCS
  Workshops in Computing series (1991).

  	Geoff.

Geoff,

It seems to me that a finished program is indeed a very formal spec of
what needs to be done.  Read a program, and deduce backwards
from it *exactly* what the requirements are.  The 20000 lines of code
are my "food mixer" label, and if it doesn't play your CD...

Now what is wrong with this approach that is also not
wrong with formal specifications?

  /Mukesh

Mukesh,

> It seems to me that a finished program is indeed a very formal spec of
> what needs to be done.  Read a program, and deduce backwards
> from it *exactly* what the requirements are.

> Now what is wrong with this approach that is also not
> wrong with formal specifications?

1. In the general case you can't do this. Most "conventional" programming
languages don't have formal semantics, therefore you are always at risk of
finding some part of the program whose meaning is ambiguous. From this point on
you cannot know what the original author intended.

2. Even if the language in question has a formal semantics which is small
enough to be understood, it is much more difficult to do it this way. A program
contains large quantities of detail which are essential to the implementation
but irrelevant to the specification. When you read a well written formal
specification it describes only what is required. When you read a similarly
well written program, there is all the irrelevant (to the specification) detail
interleaved with the (small) amount of "specification". This makes it
substantially harder to extract the intended specification.

	This is akin to observing that by reading the output from an AXP
compiler you "should" be able to work out what the program is doing. Well maybe
you can, (I've never done it) but it would be a _lot_ easier to read the source
code.

3. You can't reason about a program. You can prove properties of a formal
specification to probe its accuracy, completeness and so forth. You may also be
able to prove that an alleged implementation is a correct refinement of this
specification. None of this is possible with just a program. Worse, if all you
have is a program, then there isn't even a functional specification in English
(or whatever) and the code you are reading was just hacked into the machine
without any serious forethought.

	What it comes down to is using the right tool in the right place. A
formal specification language is the right tool (I claim) to describe _what_ is
wanted. A programming language is the right tool to tell the computer _how_ to
do it. Since the two are different the author has (should have?) an obligation
to prove that the two different descriptions are equivalent. If the spec is in
English this obligation is impossible. If there is no spec at all then one of
the tools (the programming language) has been mis-used.

	Geoff.

> languages don't have formal semantics, therefore you are always at risk of
> finding some part of the program whose meaning is ambiguous.

How can a part of the program be ambiguous?  The processor has to interpret it.

It seems like you are just using negative connotations associated with "typing
straight into the terminal" and "hacking" to somehow lead to the conclusion that
programming languages are not formal.  But even the worst programmer cannot
write ambiguous programs, though the programs might not do what they are
supposed to do!  This might be a subtle distinction, but very important to this
discussion and the root of our disagreement, I think.

I think there are many ways to improve program quality -- use of good languages,
good methodologies, design & code reviews, iterative prototyping, quality
testing.  I also think program verification falls in this category.  It is a
matter of degrees, and not a black & white differentiation.

The what vs how by itself is not a very good distinction, since there are many
levels involved, and the "what" of one level is the "how" of next level.

If done right, a formal language might provide high level specifications easiER
to write/read than writing/reading code, and hence more useful.  That's what led
to my conclusion that program verification should be considered as methods of
improving programming, not proving.  Ultimately, the success of program
verification methods would be measured by how easy to use are the tools which
come out of this field.

/Mukesh

    OK You want a simple ambiguous program. Here is one.
    
    WITH cd_player;
    WITH food_processor;
    WITH text_io;
    
    PROCEDURE main IS
    
            half    : CONSTANT := 0.5;
    
    BEGIN
            IF integer(half) = integer (half) THEN
    		text_io.put_line("I am a food_processor.");
    		food_processor;
            ELSE
    		text_io.put_line("I am a CD player.");
    		cd_player;
            END IF;
    END main;
    
    At first this program is obviously a food processor. After all 0.5 =
    0.5. However the Ada Language Reference Manual Clearly states that 0.5
    can round to 0 or 1 when converted to an integer. Whats more it states
    that this behaviour is non-deterministic - just because you got 0 last
    time doesn't mean you'll get 0 this time. So you have (0=0), (0=1) and
    (1=1).
    
    Naturally almost all compilers� will make a decision one way or the
    over (always round up or always round down) so you'll always get (0=0)
    or (1=1) and you'll always be a food processor. Indead if you look at
    the Alpha AXP machine output (or VAX for me :-( ) then `cd_player` has
    probably been optimized away completely.
    
    All this goes to show that the program is not a formal specification of
    a requirement just a bug ridden interpretation written is a poorly
    defined programming language.
    
    	Rik
    
    PS If you think I picked Ada 'coz its not well defined take a look at
    your C compiler some time. Pascal is no better - see `Ambigities and
    insecurities in the ISO Pascal Standard` by Brian Wichmann.
    
    PPS If all you want is some form of program anotation then look at ANNA
    - An Annotation method for Ada.
    
    �There is an educational compiler which deliberatly uses a random
    function for this kind of thing !

Also note that

   a := b + c;

is ambiguous because it can produce different results on 8 bit, 16-bit and
32-bit computers, causing overflow on some and not on others.  Before one can
unambiguously determine the results, one must have sufficient information about
the environment the program will execute in.

But I am sorry Rik, this does not appear to me to illustrate any particular
point.  Unless you are claiming that the whole point of formal languages is to
cover boundary conditions (like .15).  If that is the claim, then formal
languages should be viewed in that light, of course.  But I am not sure the
claim or the direction is so limited.

  /Mukesh

/Mukesh

> Also note that

>   a := b + c;

> is ambiguous because it can produce different results on 8 bit, 16-bit and
> 32-bit computers, causing overflow on some and not on others.  

	Completely true. Another example of the problem. A formal language
wouldn't have this problem in that it would state quite clearly what number
ranges were involved.

> Before one can unambiguously determine the results, one must have sufficient
> information about the environment the program will execute in.

	But I don't want to know what the results are. I want to know what the
program is supposed to do. Why don't you know? If you had a decent
specification you would know. Apparently, to answer the question "what is this
program supposed to do" you have to know who's compiler you are using, how they
interpreted the language description, what operating system you are running on,
what hardware platform ... (the day of the week maybe? but I digress ...) And
all I want to know is "what is this program _supposed_ to do".

	From one of your previous replies.

> Read a program, and deduce backwards from it *exactly* what the requirements
> are.

	OK. Lets do that with a slightly modified version of Rik's program.

    WITH cd_player;
    WITH food_processor;
    WITH text_io;
    
    PROCEDURE main IS
            half    : CONSTANT := 0.5;
    BEGIN
            IF integer(half) = 0 THEN
    		text_io.put_line("I am a food_processor.");
    		food_processor;
            ELSE
    		text_io.put_line("I am a CD player.");
    		cd_player;
            END IF;
    END main;

	Now the problem is "read _this_ program, and deduce backwards from it
*exactly* what the requirements are". Go ahead. Have a nice day. Off the top of
my head I can think of two, quite different, valid sets of requirements this
might satisfy. Someone else might be able to suggest some others. Which is the
"right" one? You don't know. Your only hope for finding out is a) ask the
author (gee, that's certainly a reliable technique) b) hope that you know what
the platform is, hope that you have the platform available (with all the same
versions of course), run the program and hope that the behaviour you see in
your test case(s) is representative of _all_ cases. What use is this? I want a
specification to tell me what the program is to do.

	To summarise again. The value of a formal language and specification is
that

1. You can precisely describe _what_ is wanted without reference to how that is
to be achieved. Without a formal language it is very hard to be precise.

2. You can explore the quality of that specification by reasoning about it (ie
doing proofs). This is impossible without a formal language.

3. You can prove (or disprove) that an alleged implementation satisfies the
original specification. This is also impossible without a formal specification.

	One thing puzzles me here. Forget about formal methods for a moment. Do
you even think that a specification is a good idea? Your suggestion that it is
possible to deduce requirements from code suggests that you don't think a
separate specification is necessary, but maybe I'm reading too much into one
idea. If you think a requirements document is unnecessary - however it is
written - then you certainly won't want a formal spec. However, if you do think
a specification is worthwhile then why wouldn't you want a better one?

	Geoff.

Let me restate the central objection, before we start
chasing down irrelevant details.

I am disputing that the "formal specifications" are necessarily
a correct translation of the "actual requirements".

You are getting around this by defining the "actual requirements"
to be whatever the writer of formal spec turned out.

So let us consider a few questions.  It could be I just don't
know enough about formal languages, so let us get your
claims straight:

1)  Is it possible to have errors in a specification written
    in a formal language?  Could the author ever say "Oops,
    I misunderstood, I will have to rewrite this part of the spec?"

2)  Is it possible to have an ambiguity in a formal language?

3)  Does a formal language specify the ranges to
    be used for integer values, floating point
    numbers, and character sets?

>> Also note that
>>   a := b + c;
>> is ambiguous because it can produce different results on 8 bit, 16-bit and
>> 32-bit computers, causing overflow on some and not on others.  
>	Completely true. Another example of the problem. A formal language
>wouldn't have this problem in that it would state quite clearly what number
>ranges were involved.


If all the formal language is doing is to cover cases like
this, I would not have the least interest in it.  As a matter
of fact, I would prefer that things at this level of detail
*not* be spec'd out.  Because if they are, the spec is
only good for one particular machine, and even there,
may unnecessarily require foregoing many of the hardware
operations provided by the machine.

If the formal spec says integers are limited to -16767 to 16768,
I have to make sure that whenever I add two numbers on an 18
bit machine, I check for ranges (without being able to use
the hardware's capability to check for overflow).  If the formal
spec (or my "deduced backwards" spec) refuses to specify to this
level of detail, I can leave addition to the hardware
and have things work quite well.

    One point not brought out in this discussion (but alluded to in one of
    th replies) is that preconditions / postconditions are NOT restricted
    to referring to the parameters.
    
    They can be predicates on "the state of the system".  This includes
    global variables, files on disk, status of some LED on the front panel,
    whatever...
    
    You can also define "system" to encompass distributed systems.  Here
    state includes the state of all members of the distributed system. 
    Since you're in an abstract world, youre omnicient and can see a
    consistent picture of global state.
    
    For reasoning purposes, you can also define state to include
    information not maintained by any reasonable program.  For example, you
    might keep around "state" like a complete history of some "event" in
    the system that have occured so you can reason about whether or not
    duplicate events ever happen.
    
    Steveg