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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: =?utf-8?B?QWNjZXNzIHRvIHN1YuKAkXByb2dyYW0gYXMgYXJndW1lbnQ6IGZpcnN0IG8=?= =?utf-8?B?cmRlciBvciBoaWdoZXIgb3JkZXI/?= Date: Thu, 17 Apr 2014 07:39:34 +0200 Organization: Ada @ Home Message-ID: References: NNTP-Posting-Host: ZSRdFONJ4IDiiOWDstzEDA.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/12.16 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:19343 Date: 2014-04-17T07:39:34+02:00 List-Id: Le Fri, 27 Dec 2013 19:24:24 +0100, Yannick Duch=C3=AAne (Hibou57) = a =C3=A9crit: > Hi all, =E2=80=A6 it's a long time I did not asked a question here. Al= so, Merry = > Christmas to all, although I'm a bit late. > > Just a quick question with a formal taste: within Ada, functions and = > sub=E2=80=91programs are not treated as values or expressions; within = functional = > programming, a function getting a function as an argument, is an highe= r = > order function (precisely, second order, if I'm not wrong); within Ada= , = > is a sub=E2=80=91program which get a access to a sub=E2=80=91program, = still to be named = > a first=E2=80=91order sub=E2=80=91program or an higher=E2=80=91order s= ub=E2=80=91program instead? > > Surely the best way to get an answer to this, is to get an answer to = > this other one: what do you need to prove something about an Ada = > sub=E2=80=91program getting an access to another sub=E2=80=91program a= s an argument? = > First Order Logic or Higher Order Logic? I've never played with it, an= d = > don't remember if, as an example, SPARK allows it, neither I know if = > SPARK if finally based on FOL or HOL. > > If someone already did this: if you ever proved something about such a= = > sub=E2=80=91program, what kind of logic have you used? I lately found an answer to this question:=E2=80=AFit's an extended FOL = (which is = does not seems to be HOL). http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-November/001= 532.html Quoting Yannick Moy, who worked on both Frama=E2=80=91C and SPARK/Ada: > 2) The specification languages are quite different too. ACSL allows > expressing axiomatizations directly at the level of the C program, whi= le > SPARK only allows declaring proof functions, which must be axiomatized= = > with > Prolog rewrite rules in a separate file. SPARK defines #own variables = = > that > are used for hiding and refinement. ACSL defines state labels that can= be > used to denote a program point in logic functions and predicates. To = > answer > a question in a following email, **both are supersets of first-order = > logic**, > but quite different from each other. -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity