Access to sub‑program as argument: first order or higher order?

Access to sub‑program as argument: first order or higher order?

[Yannick Duchêne (Hibou57)]

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

Re: Access to sub‑program as argument: first order or higher order?

[Yannick Duchêne (Hibou57)]

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