Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 27.06.12 15:41, Nasser M. Abbasi wrote:
> I did not check, but I assumed all along that the evaluation
> of pre() can have no side effects?

Perhaps evaluating Pre's expression has exactly the
side effects that the programmer intends it to have.

It is not even necessary to infiltrate the expression
with side effects to make it harmful. They can well
be pure, see below.

If you want to be a wicked programmer using a reliable
language for doing evil things reliably, use Ada:
write a function K, presumably constant and omit a post
condition that affirms its constant result. Or, specify the
postcondition and make it appear to be constant when
it isn't,  A suitably redefined "=" can modify its arguments:

   with Post => K'Result = 123.

In any case, if what K returns is a random number,
refer to this "constant" function K in

   procedure P (X : Natural)
      with Pre => (X < K);


This issue with Pre's programmer isn't different from side effects
he or she puts in pragma Assert, or, more generally, anywhere
a non-static expression is allowed to do what the programmers
want it to do.

Indeed, using more pure, "functional" approach,
define ">" to return true when its left argument = 0.
Then side effects are not needed for wreaking havoc:

   function ">" (left, right: Natural) return Boolean is
   begin
      return left = 0;
   end ">";

   if Y > 0 then
      return F (X / Y);
   end if;