search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
47 stars 8 forks source link

Clarification on order of arguments for termination measure #79

Closed zilbuz closed 3 years ago

zilbuz commented 3 years ago

In the termination paragraph (2.5), the order of arguments for the measure is not clear.

The equivalence R(x, y) <==> x > y && x >= 0 for the integer measure (§2.5.1) uses the first argument x as the previous value, but the example lexico(intpair p1, intpair p2) in the general measure (§2.5.2) seems to use the second argument p2 as the previous value as the definition of the predicate is similar to p2 > p1 && p2 >= 0.

What is the correct order of arguments?

pbaudin commented 3 years ago

Unfortunately, there is a typo in the example. That is fixed by e0da6be76 commit.