* Access to sub‑program as argument: first order or higher order?
@ 2013-12-27 18:24 Yannick Duchêne (Hibou57)
2014-04-17 5:39 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 2+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-12-27 18:24 UTC (permalink / raw)
Hi all, … it's a long time I did not asked a question here. Also, Merry
Christmas to all, although I'm a bit late.
Just a quick question with a formal taste: within Ada, functions and
sub‑programs are not treated as values or expressions; within functional
programming, a function getting a function as an argument, is an higher
order function (precisely, second order, if I'm not wrong); within Ada, is
a sub‑program which get a access to a sub‑program, still to be named a
first‑order sub‑program or an higher‑order sub‑program 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‑program
getting an access to another sub‑program as an argument? First Order Logic
or Higher Order Logic? I've never played with it, and 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‑program, what kind of logic have you used?
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Access to sub‑program as argument: first order or higher order?
2013-12-27 18:24 Access to sub‑program as argument: first order or higher order? Yannick Duchêne (Hibou57)
@ 2014-04-17 5:39 ` Yannick Duchêne (Hibou57)
0 siblings, 0 replies; 2+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2014-04-17 5:39 UTC (permalink / raw)
Le Fri, 27 Dec 2013 19:24:24 +0100, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> Hi all, … it's a long time I did not asked a question here. Also, Merry
> Christmas to all, although I'm a bit late.
>
> Just a quick question with a formal taste: within Ada, functions and
> sub‑programs are not treated as values or expressions; within functional
> programming, a function getting a function as an argument, is an higher
> order function (precisely, second order, if I'm not wrong); within Ada,
> is a sub‑program which get a access to a sub‑program, still to be named
> a first‑order sub‑program or an higher‑order sub‑program 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‑program getting an access to another sub‑program as an argument?
> First Order Logic or Higher Order Logic? I've never played with it, and
> 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‑program, what kind of logic have you used?
I lately found an answer to this question: it's an extended FOL (which is
does not seems to be HOL).
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-November/001532.html
Quoting Yannick Moy, who worked on both Frama‑C and SPARK/Ada:
> 2) The specification languages are quite different too. ACSL allows
> expressing axiomatizations directly at the level of the C program, while
> 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.
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2014-04-17 5:39 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-12-27 18:24 Access to sub‑program as argument: first order or higher order? Yannick Duchêne (Hibou57)
2014-04-17 5:39 ` Yannick Duchêne (Hibou57)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox