Unsatisfiable spec of square root function

[mick62]

Description

Only partial satisfiable spec for square root function in Web documentation.

Steps to Reproduce

Documentation on http://overturetool.org/languages/
Text:
"For example, a function SQRT for calculating a square root of a natural number might be defined as follows: ... "

Expected behavior:

A general satisfiable specification defines an eps > 0 for the distance between x and r*r, i.e.

SQRT(x:nat) r:real
post abs(r*r - x) <= eps

Actual behavior:

Text:
SQRT(x:nat) r:real
post r*r = x

The problem with this definition is that the postcondition can only be fulfilled when x is a square number a^2 like 4. But for all other (i.e. non-square) numbers, function SQRT can not terminate because the type of real numbers is assumed as having unlimited precision. The process of calculating e.g. sqrt(2) can not end in finite time as the mathematical object sqrt(2) has infinite many digits.

[nickbattle]

You make an interesting point. But I think that pure VDM is unlimited precision. Of course any implementation would have finite precision in an interpreter, but should a pure specification really take that into account?

(Incidentally, there is an arbitrary precision build of VDMJ available, but it is still finite precision).

[mick62]

Of course the post conditionpost r*r = x could be interpreted in the sense of a mathematical limit ("limes").lim[t -> infinity] r*r -> x i.e. for every desired value eps > 0, there is finite time t in which a value r can be computed such that abs(r*r - x) < eps. But then SQRT is no longer a function in the regular sense. To make this explicit, the post condition could be post r*r -> x This limes notation would then integrate purity (simplification through abstraction) and reality (infinite calculation time).It would avoid mentioning explicitely the eps distance bound, but would implicitly incorporate eps as part of the limes mechanism. Now you have to extend VDM!Good luck. Gesendet von Yahoo Mail auf Android Am Fr., Juni 14, 2019 at 23:46 schrieb Nick Battle<[email protected]>: You make an interesting point. But I think that pure VDM is unlimited precision. Of course any implementation would have finite precision in an interpreter, but should a pure specification really take that into account? (Incidentally, there is an arbitrary precision build of VDMJ available, but it is still finite precision). — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[nickbattle]

Interesting. I hadn't come across Limes notation, though it is only mentioned in German web pages - do you just mean limit notation?

You might be on to something here. I can see the value of a clear mathematical statement that describes something precisely that accounts for the imprecision of an implementation. But we would have to think through where it could be sensibly applied in the specification language (and define its semantics, of course).

There is a mechanism for proposing language changes, via the Language Board. It can be a lengthy process, but several changes have been successfully made over the years. The onus is on the person proposing the change to define something that is adequate; the Language Board isn't there to solve problems, but to manage the change process. See LB wiki.

[peterwvj]

Since VDM is unlimited precision, changing the language to address this issue feels wrong. That being said, I do agree that a notation for expressing limits could be useful. Just a crazy thought: to void changing the language itself, would it be possible to use the annotations feature to create something useful? Perhaps something that would enable users to express function limits by adding annotations such as @Limit(r * r, x) in their specs.

[nickbattle]

It would certainly be possible to create an annotation, but what functionality would it have - is there a proof obligation associated with the limit?

[peterwvj]

I'm not sure, but my point is just that you could use it to implement the same functionality that a new language feature would contribute. Syntax validation would be helpful, perhaps it would produce a PO like you suggest, perhaps integration with some other tool more suitable for these analyses etc. It was just a thought.