--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on March 2009 ---
Sorry for the unclear answer about this. Pascal is right. Let me rephrase that in a general setting: if you annotate //@ decreases V(x1...xk) for R f(x1,..,xk) { .... f(e1,...e_k); ...} then the VC at the recursive call will be //@ assert V(e1,..,ek) R V(x1...xk) for the well-founded order R . By default, R is the relation R(x,y) on integer defined by 0 <= y && x < y. This is the most convenient well-founded order on ints. (more details in ACSL ref man in section 2.5 http://frama-c.cea.fr/download/acsl_1.4.pdf) Pascal Cuoq wrote: >> I don't understand the assert clause in the code below: >> - "0 <= n" follows from the precondition >> - "n-1 < n" is a tautology >> So the assert clause should always evaluate to true, irrespective of >> what the program does? > > The assertion is there to illustrate how decreases clauses will > work when they are supported. > > If the decreases clause had been supported by Jessie, it would > have been translated into a verification condition very much like > the property 0 <= n && n-1 < n; to be proved at the point of the assert. > > The fact that the property holds means that the decreases clause is a > valid one, > and consequently that the termination of the function is guaranteed. > > Pascal > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |