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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: "functional" programming in Ada
Date: Fri, 09 Mar 2018 08:40:06 +0000
Organization: A noiseless patient Spider
Message-ID: <lytvtphcbd.fsf@pushface.org>
References: <p7luc6$fu7$1@dont-email.me>
	<896b83c6-83d4-4ffc-8c56-1481802ea8fd@googlegroups.com>
	<961c82e0-7d7e-48af-8751-916a3332ccc5@googlegroups.com>
	<1520428274.2488.155.camel@obry.net>
	<p7qb11$hi0$1@franka.jacob-sparre.dk> <p7qrun$461$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="bee047c6f69586d2576a0898a85dfda1";
	logging-data="9708"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+/g43Mm4zv9ClkV085ddf4kkIiIlzKAEw="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (darwin)
Cancel-Lock: sha1:keH6Fj8OgbylklTYwS63rWo/H7s=
	sha1:RtU/c6JpjEHH9LMO2MZK8P0hgXU=
Xref: reader02.eternal-september.org comp.lang.ada:50906
Date: 2018-03-09T08:40:06+00:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> On 08/03/2018 04:34, Randy Brukardt wrote:
[...]
>> The various contracts (preconditions, postconditions, predicates,
>> etc.) all contain some executable code, and it is necessary for
>> callers to be able to understand those contracts. Expression
>> functions help in this, while the bulk of the implementation should
>> remain in the body.
>
> These are not contracts if have any executable code, and more
> importantly, understanding cannot be achieved by exposing
> implementation/code.
>
> P.S. Contracts exist prior the program (programs, actuall) and surely
> prior to any execution of (any implementation of any programs under
> the contract).

When I was taught VDM (a long time ago, and never put to actual project
use) we wrote what are essentially contracts. You'd be left to implement
the corresponding code following the contracts.

Pre/postconditions etc correspond to these contracts, in a potentially
executable form, and I'm going to call them contracts as a convenient
shorthand (as in the Rationale).

As you know, the meaning of the program mustn't depend on actually
executing the contracts, and the default GNAT behaviour is not to
generate executable code for them (I don't know whether expression
functions which are only involved in contracts actually generate object
code, but one would hope they'd be eliminated by compiler analysis).

An expression function in the spec has to help in understanding what the
contract says. I wondered whether it might correspond to a lemma? ("a
subsidiary proposition , proved for use in the proof of another
proposition").