From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: mheaney@ni.net (Matthew Heaney)
Subject: Precondition Checking For Ada 0X (Was: Separation of IF and Imp:
 process issue?)
Date: 1997/09/10
Message-ID: <mheaney-ya023680001009971956580001@news.ni.net>#1/1
X-Deja-AN: 271484194
References: <33E9ADE9.4709@flash.net>
 <mheaney-ya023680000409972313230001@news.ni.net>
 <5upe9k$7he@newshub.atmnet.net>
 <mheaney-ya023680000609971422530001@news.ni.net>
 <5utag9$o6s@newshub.atmnet.net> <3416ad14.0@news.uni-ulm.de>
 <3416D889.4A6C@pseserv3.fw.hac.com>
Organization: Estormza Software
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-09-10T00:00:00+00:00
List-Id: <comp.lang.ada>



In article <3416D889.4A6C@pseserv3.fw.hac.com>, "W. Wesley Groleau x4923"
<wwgrol@pseserv3.fw.hac.com> wrote:


>I claimed before (perhaps wrongly) that adding assertions to Ada
>seemed fairly trivial, but even if correct, there is one aspect
>that would NOT be trivial.  Since an Eiffel-style assertion is
>part of the contract, BUT it is executed when a routine is called,
>how can it be put in an Ada spec in a form that is compilable AND
>associated with a particular declaration?

You'd probably have to change the syntax of subprogram declarations. 
Here's an example:

type Root_Stack is abstract tagged private;

function Empty (Stack : Root_Stack) return Boolean;

function Full (Stack : Root_Stack) return Boolean;

procedure Pop
  (Stack : in out Root_Stack)
precondition
   Not_Empty: not Empty (Stack);
end Pop;

function Top 
  (Stack : Root_Stack) return Stack_Item
precondition
   Not_Empty: not Empty (Stack);
end Top;

procedure Push
  (Item : in     Stack_Item;
   On     : in out Root_Stack)
precondition
   Not_Full: not Full (On);
end Push;



or consider a sequence abstraction:

type Root_Sequence is abstract tagged private;

function Length 
   (Sequence : Root_Sequence) return Natural;

procedure Remove_Item
  (Sequence : in out Root_Sequence; 
   Index        : in        Positive)
precondition
   Is_Present: Index <= Length (Sequence);
end;

You get the idea.  The subprogram precondition is a list of boolean
expressions that are functions of one or more of the subprogram arguments. 
The precondition (and postcondition too - I didn't show that) is part of
the signiture of the subprogram.

When the call happens, the actual parameters are calculated, and then the
preconditions are evaluated; a precondition violation (a boolean expression
whose value is False) would cause Constraint_Error to be raised (or
whatever), just as for actual parameters that don't satisify range
constraints of the formal parameters.

A simple example of a postcondition would be

function Length
  (Sequence : Root_Sequence) return Integer
postcondition
   Length >= 0;
end;

(though of course this example is possible using existing Ada mechanisms).

I still have to think about how to state a representation invariant.  Its
specification would somehow have to be attached to the full view of the
type, and would be evaluated at exit from a subprogram.

I also haven't thought of a convenient way to state a postcondition in
terms of a change in a value (ie the length before the call versus the
length after the call).

This is my first cut at an extended syntax for Ada 0X.  Any opinions?

--------------------------------------------------------------------
Matthew Heaney
Software Development Consultant
<mailto:matthew_heaney@acm.org>
(818) 985-1271