Re: Operation can be dispatching in only one type

Dmitry A. Kazakov schrieb:
On Tue, 08 Dec 2009 11:06:54 +0100, Georg Bauhaus wrote:

Dmitry A. Kazakov schrieb:
In my view pre-/postconditions and
invariants should be static, used strictly for program correctness proofs.
Subtypes should complement them for dynamic run-time checks (recoverable
faults).
Hm. What would be your subtype based expression for

generic
type E is private;
package Stacks is

type Stack is private;

procedure push (Modified_Stack : in out Stack;
Another : Element)
with pre => not Full (Modified_Stack),
post => Size (Modified_Stack'Exit) = Size (Modified_Stack);

procedure pop (Modified_Stack : in out Stack)
with pre => not Empty (Modified_Stack),
post => Empty (Modified_Stack);

None. The above is wrong. You cannot implement this contract (if we deduced
one from the given pre- and postconditions). Proof:

loop
Push (Stack, X);
end loop;

q.e.d.

Therefore the contract of a stack must always contain ideals, e.g.

1. exceptions, like Full_Error, Empty_Error;

I understand that exceptions are implied by Eiffel style
conditions.

The Eiffel camp might answer, for example,

Lock (Stack);

while not Full (Stack) loop
Push (Stack, X);
end loop;

Unlock (Stack);

q.e.d.

2. blocked states, like holding the caller until the stack state is changed
from another task.

Would you want this to be possible with Ada, or with SPARK? ;-)


Pre- and psotconditions are to be used to prove a contract to hold. They
themselves are no contract.

In Eiffel, pre post and inv are used to write a contract.
The proof obligation rests on the programmer.
.

Relevant Pages

  • Re: Operation can be dispatching in only one type
    ... Subtypes should complement them for dynamic run-time checks (recoverable ... procedure push (Modified_Stack: in out Stack; ... Therefore the contract of a stack must always contain ideals, ... The proof obligation rests on the programmer. ...
    (comp.lang.ada)
  • Re: Operation can be dispatching in only one type
    ... used strictly for program correctness proofs. ... Subtypes should complement them for dynamic run-time checks (recoverable ... procedure push (Modified_Stack: in out Stack; ... Therefore the contract of a stack must always contain ideals, ...
    (comp.lang.ada)
  • Re: I want to learn forth but...
    ... on each pass of the loop. ... deeper in the execution stack. ... faster than even a register bank of any real size. ...
    (comp.lang.forth)
  • Re: DISFAVORED Was: name for 3 PICK finally?
    ... No complication except having a pool for stack variables, ... I felt like it was nice to have a loop ... I also have a defining word called PLURAL which I use to make plurals ... actually need any headerless definitions, ...
    (comp.lang.forth)
  • Re: How would you do this in forth?
    ... then compiles the address as a literal. ... stack so you can do something interesting with it later during run ... and execute it with yield. ... so no more dangerous than BEGIN WHILE THEN or DO LOOP;) ...
    (comp.lang.forth)