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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: "functional" programming in Ada Date: Fri, 9 Mar 2018 14:39:26 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <896b83c6-83d4-4ffc-8c56-1481802ea8fd@googlegroups.com> <961c82e0-7d7e-48af-8751-916a3332ccc5@googlegroups.com> <1520428274.2488.155.camel@obry.net> NNTP-Posting-Host: MyFhHs417jM9AgzRpXn7yg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0 Content-Language: en-US X-Notice: Filtered by postfilter v. 0.8.3 Xref: reader02.eternal-september.org comp.lang.ada:50907 Date: 2018-03-09T14:39:26+01:00 List-Id: On 09/03/2018 09:40, Simon Wright wrote: > "Dmitry A. Kazakov" 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