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.241.162 with SMTP id wj2mr16058288pbc.2.1341659903161;
        Sat, 07 Jul 2012 04:18:23 -0700 (PDT)
Path: 
 l9ni11068pbj.0!nntp.google.com!news1.google.com!goblin3!goblin1!goblin.stu.neva.ru!noris.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Sat, 07 Jul 2012 13:17:52 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:13.0) Gecko/20120614 Thunderbird/13.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>
 <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <jrsmfh$6fq$1@speranza.aioe.org>
 <npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net> <js00co$clj$1@munin.nbi.dk>
 <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <js2hq5$9fj$1@munin.nbi.dk>
 <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <jsttoc$hc2$1@munin.nbi.dk>
 <13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net> <jt2thn$1hr$1@munin.nbi.dk>
 <13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net> <jt80n3$gjh$1@munin.nbi.dk>
 <1ee9qp0cy5me4.1vh22pi92ls6n$.dlg@40tude.net>
In-Reply-To: <1ee9qp0cy5me4.1vh22pi92ls6n$.dlg@40tude.net>
Message-ID: <4ff81ae0$0$9504$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 07 Jul 2012 13:17:52 CEST
NNTP-Posting-Host: 2ce553e6.newsspool1.arcor-online.net
X-Trace: 
 DXC=f7ObF6[3?Q=^8FBo0_81f>ic==]BZ:af>4Fo<]lROoR1nkgeX?EC@@0>UoMUM1ISk?PCY\c7>ejV8fT71]<6`cN;E919Rge1a85
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-07-07T13:17:52+02:00
List-Id: <comp.lang.ada>

On 07.07.12 10:06, Dmitry A. Kazakov wrote:
>> Contract is roughly equivalent to (Ada) specification. Implementation is
>> roughly equivalent to (Ada) body.

> There are two kind entities involved A and
> B. The check may be attributed to either A or B.

There is no need for such attribution. Indeed, assertion monitoring
(note the word) ideally works like in the following illustration.

Monitoring here uses a monitoring processor (not an Ada thing,
but a conceptual thing to which an Ada compiler can supply suitable code).
Let there be a procedure that adds 42 to its argument (in out) unless
adding 42 makes the result too large. Let the argument be passed in r1.

add_42:
         load    $2A, r2           # 42 in r2
         add     r2, r1            # X := X + 42;
         *return

call_add_42:
         load    $0, r1            # X := 0;
         *call   add_42            # Add_42 (X);
         store   r1, (#output)     # print X
         *return

The monitor can be turned on or off. The special instructions [X]call
and [X]return can be monitored.  When monitoring is on, then an
auxiliary processor is hooked up to *call and/or *return. It can
read all data that the program can read, too.

When monitoring, any *call or *return will make the monitor evaluate
the corresponding assertions. If they are true, the system continues
executing the program. If they are false, the system prints a diagnostic
message and stops.

If "r1 is too large" means "r1 > 968", then this is the assertion associated
with calling add_42.  The monitor will test the assertion when "*call add_42"
is the next instruction to be performed, and monitoring of calls has
been  turned on.

The point is that the "program proper", i.e. the list of instructions,
is the very same irrespective of monitoring assertions.