Re: "functional" programming in Ada

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 09/03/2018 09:40, Simon Wright wrote:
> "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).

Proper pre/post conditions are propositions to be used ("executed") in 
the logical inference/proof. They define the contract.

If an expression is used to define a contract, that contract is 
obviously undefined until the expression evaluated.

> 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).

And if not?

> 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").

There are propositions, theorems, lemmas. And there are algorithms, 
instructions etc. The former are never the latter and conversely. 
Expression-function can be either. That depends on the language we are 
talking about: #1 an expression of the meta-language of contracts or #2 
an expression of the object language Ada.

Now the point is that even if an expression-function were a part of the 
language of contracts, then that is still bad idea because the language 
design principles should hold for both languages. If the meta language 
of contracts becomes so complex that it would require procedural 
decomposition, then that must be done in a sane way, with separating 
interfaces and implementations. The contract-function would have bodies 
defined elsewhere rather than clumped together with specification.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de