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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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