Hello Marek,

Ok.
I was also surprised to learn that the compiler does not check preconditions by
default.

Just append "-chk" to your sacomp statement.

It is an alias to "-chk_all all" which will make sure that all checks will occur
in all classes.
(I got that from the sacomp man page)

(BTW, thanks for asking questions, it "forces" me to look for info :-) ).

Best regards,
Fadi.

Marek Janukowicz wrote:
>
> Hello again
>
> Are pre/post conditions supported by default? I have a test program:
> class MAIN is
> [...]
>  create( a : INT ) : SAME
>    pre a < 10
>    post self.a < 5
>  is
> [...]
>  main
>    pre 1 > 2
>    post 1 > 2
>  is
> [...]
>
> and it doesn't raise any error, displaying the messages (as it should if the
> preconditions were not there). Do I need to somehow switch on with some
> compiler switch?
>
>--
> Marek Janukowicz