search

Ada-Rapporteur-Group / User-Community-Input

Ada User Community Input Working Group - Github Mirror Prototype
27 stars 1 forks source link

'Old should be applicable to a value rather than just an "object" #92

Open sttaft opened 6 months ago

sttaft commented 6 months ago

There is no particular reason that the 'Old attribute should not be applicable to a value, such as an attribute. In terms of efficiency, writing Arr'Length'Old is much more efficient than writing Arr'Old'Length in a postcondition, because the amount of information that needs to be saved is generally going to be an order of magnitude less.

At some point we should review all RM rules that require "objects" and see whether they could allow values as well.

CKWG commented 6 months ago

Hm, isn't that a question of optimization? It's clear whether in the code also Arr'Old is needed or only Arr'Old'Length. In the latter case, Arr'Old need not be kept. What's more, pre and post conditions are mainly for SPARK and thus evaluated before execution. Execution can be controlled via pragma Assertion_Policy - code in the wild happy hunting grounds will normally use Ignore. Nevertheless, the language should allow values.

sttaft commented 6 months ago

Hm, isn't that a question of optimization? It's clear whether in the code also Arr'Old is needed or only Arr'Old'Length. In the latter case, Arr'Old need not be kept.

That would be a nice optimization, but it could require significant analysis for certain attributes (not this one!).

What's more, pre and post conditions are mainly for SPARK and thus evaluated before execution.

I beg to differ on this one. Anyone who is not using pre and postconditions more generally is missing a very important feature of modern Ada, in my view.

Execution can be controlled via pragma Assertion_Policy - code in the wild happy hunting grounds will normally use Ignore.

Again, I beg to differ. Suppressing assertion checks is pretty silly, at least during development, if you are not using SPARK to check them statically. And even with SPARK, it is useful to run with assertion checking turned on before you start beating yourself up because you can't prove some of the postconditions statically, in case the postconditions are just plain wrong.

Nevertheless, the language should allow values.

Agreed on this one!