[mercury-users] Pre- and Post- conditions

[Randall Helzerman]

> Good day to all,
> 
> I'm working on the development of pre- and post- conditions for Mercury.

First of all, let me say that this is way-cool.

Second of all, let me say that I prefer the 2nd way over the 1st way.

Third, please let me make a suggestion, which is perhaps too radical
for the present, but I think deserves consideration.  Conceptually, I
think that pre and post conditions should really be part of the type
system.  A type can have 2 parts, one which is checked at compile time, and
one which is checked at run time, e.g. for your example:


:- type list(T) ---> []
                ; [T|list(T)].

:- type list6(T) ---> list(T), { list__length(list6(T),6) }.

A smart compiler might even be able to check this type at compile time
using abstract interpretation.


> Here are the 2 options that seemed me to be the most interesting ones.
> I'm waiting for your opinions and/or advises.
> In both cases, pre and post should be declared below the mode to which
> they relate.
> 
> Short examples being clearer than long explanations, here are examples of
> the 2 ways with an "append-like" predicate called append6.
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> ----------------------------------------------------------------------------
> 1st WAY :
> ----------------------------------------------------------------------------
> 
> :- pred append6(list(T),list(T),list(T)).
> :- mode append6(in,in,out).
> :- pre append6(A::in,B::in,_::out) is preapp6(A,B).
> :- post append6...
> 
> ...
> ...
> ...
> 
> :- pred preapp6(list(T),list(T)).
> :- mode preapp6(in,in). 
> 
> preapp6(A,B) :-
> 	list__length(A,X),
> 	list__length(B,Y),
> 	Z=X+Y,
> 	Z>=6.
> 
> ----------------------------------------------------------------------------
> 
> DRAWBACK(S):
> 1- You have to create a new predicate even if the precondition is very
>    simple, which is not user-friendly.
> 
> ADVANTAGE(S):
> 1- If the precondition is complex, it is more readable.
> 2- The predicate preapp6 can be used elsewhere in the program.
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> ----------------------------------------------------------------------------
> 2nd WAY :
> ----------------------------------------------------------------------------
> 
> :- pred append6(list(T),list(T),list(T)).
> :- mode append6(in,in,out).
> :- pre (append6(A::in,B::in,_::out),
> 	"list__length(A,X),
> 	list__length(A,X),
> 	Z=X+Y,
> 	Z>=6"
> 	).
> :- post...
> 
> ----------------------------------------------------------------------------
> 
> DRAWBACK(S):
> 1- Having Mercury implementation code "lost" in the declarations makes the 
>    program less readable.
> 2- Maybe more complex to implement in the compiler.
> 
> ADVANTAGE(S):
> 1- Easier to use for simple preconditions.
> 2- The 2nd way can easily "emulate" the 1st way by doing :
>    :- pre (append6(A::in,B::in,_::out),"preapp6(A,B)").
>    
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> 
> The use of pre- and post- conditions will lead to the creation of a new
> option in the Mercury compiler (something like mmc --use-pre-post ).
> Should the default be to compile with or without them ?
> 
> Thanks to all.
> 
> 
> 	Patrick
> 
> --------------------------------------------------------------------------
> mercury-users mailing list
> post:  mercury-users at cs.mu.oz.au
> administrative address: owner-mercury-users at cs.mu.oz.au
> unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
> subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
> --------------------------------------------------------------------------
>