From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b78c363353551702
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.227.67 with SMTP id ry3mr1192323pbc.8.1340867763151;
        Thu, 28 Jun 2012 00:16:03 -0700 (PDT)
Path: 
 l9ni28660pbj.0!nntp.google.com!news1.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!87.79.20.101.MISMATCH!newsreader4.netcologne.de!news.netcologne.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Thu, 28 Jun 2012 09:00:55 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:12.0) Gecko/20120428 Thunderbird/12.0.1
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net>
 <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net>
 <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net>
 <Pine.LNX.4.64.1206251438390.12735@medsec1.medien.uni-weimar.de>
 <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net>
 <Pine.LNX.4.64.1206251734140.12735@medsec1.medien.uni-weimar.de>
 <bdpvyb9h7rvt.zbq0kbiq72wj.dlg@40tude.net>
 <Pine.LNX.4.64.1206261316320.22921@medsec1.medien.uni-weimar.de>
 <xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net>
 <4fe9bde5$0$6566$9b4e6d93@newsspool4.arcor-online.net>
 <z27igg6796oj$.oefrs9mmhzok$.dlg@40tude.net>
 <4fe9e7c5$0$6567$9b4e6d93@newsspool4.arcor-online.net>
 <xiqck4ormiak.xek6it0sxpq9.dlg@40tude.net>
 <4feac313$0$9504$9b4e6d93@newsspool1.arcor-online.net>
 <1et105d0sks1i.pcgog9ym17ym.dlg@40tude.net>
 <4feae0d1$0$6568$9b4e6d93@newsspool3.arcor-online.net>
 <2klq69d4qqsp$.veefi8i6jnwa.dlg@40tude.net> <jsf2j2$iif$1@speranza.aioe.org>
In-Reply-To: <jsf2j2$iif$1@speranza.aioe.org>
Message-ID: <4fec0124$0$6552$9b4e6d93@newsspool4.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 28 Jun 2012 09:00:52 CEST
NNTP-Posting-Host: c1566068.newsspool4.arcor-online.net
X-Trace: 
 DXC=l;?0R\mCUM7RadXUBHgFh34IUK<Cl32<14Fo<]lROoR18kF<OcfhCO;TUUbab]\[C<PCY\c7>ejV8_Yl<A8VPPY;WjXR__W]@V;
X-Complaints-To: usenet-abuse@arcor.de
X-Received-Bytes: 3405
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-06-28T09:00:52+02:00
List-Id: <comp.lang.ada>

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;