Pre- and Post- conditions

[Patrick KREPS]

Good day to all,

I'm working on the development of pre- and post- conditions for Mercury.
For memory, pre- and post- conditions of a certain procedure can be used
to test conditions on the input and output arguments.  These can be
replaced by the following pseudo-code :
( 
(precond) ->
	(procedure body),
	(
	(postcond) ->
		ok(end_of_call)
	;
		error(post_fail)
	)
;
	error(pre_fail)
).

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