[SystemSafety] "Ripple20 vulnerabilities will haunt the IoT landscape for years to come"

[Roderick Chapman]

On 02/07/2020 15:51, Olwen Morgan wrote:
>
> AFAI recall, recursion is banned in the SPARK subset.
>
Recursion is banned in SPARK83 through SPARK2005.

It is allowed in SPARK2014.

> But, considering that a compiler for a functional language may convert 
> tail recursion to iteration, I ask whether anything in the Ada 
> standard explicitly forbids an Ada compiler from implementing 
> iteration by recursion?
>
Not sure... but I have never seen a compiler do this.

Note again - things changed a bit with SPARK2014...

SPARK83 - SPARK2005 did not directly support proof of termination of 
loops, so all proof was "partial".

SPARK2014 _does_ support proof of termination (for loops) through a 
user-defined "Loop_Variant" expression. Not sure about what happens with 
termination of recursive subprograms, though - I'm a bit out of the loop 
with those details. The current SPARK user guide should have more... 
yeah.. see

https://docs.adacore.com/spark2014-docs/html/ug/en/source/assertion_pragmas.html#loop-variants 


> Also when did the Ada standard start using the 
> implementation-defined/unspecified/erroneous classification that 
> blights the C standard? Did it not start out with the same 
> classification as Pascal, namely 
> implementation-defined/implementation-dependent/error?
>
An entertaining historical oddity:

Ada83 used the terms "Implementation-defined", 
"Implementation-dependent", and "Erroneous behaviour"

Ada95 changed "Implementation-dependent" to "Unspecified" but left 
"Erroneous behaviour" as it is (with roughly the same meaning as 
"undefined behaviour" in C).

You'll have to ask someone much old than me why this came out this way...

  - Rod