For some functions, there may be cases in which objects
that are permitted to be modified are not modified.
An lcpp-primary starting with unchanged asserts that
its argument objects are not mutated (see section 6.2 Mutation).
For example, unchanged(a) means that,
if a were assigned in the pre-state, then it has the same abstract
value in the post-state as in the pre-state
(and if it were allocated but not assigned in the pre-state,
then it did not become assigned in the post-state).
The lcpp-primary unchanged(everything)
asserts that no object is mutated.
Such lcpp-primary forms can only be used in a postcondition.
For example, unchanged(t1,reach(t2)) asserts that
t1 and all objects reachable from t2 are not mutated
(and not deallocated).
As another example, given a specification of BankAccount
(which itself includes a specification of Money),
the following specification says that if in a call withdraw(x,m)
the value of m is greater than the value of the credit
field in the value of x, then the call has no effect.
// @(#)$Id: withdraw.lh,v 1.10 1997/07/30 04:55:02 leavens Exp $
#include "BankAccount.lh"
extern void withdraw(BankAccount& a, Money amt) throw();
//@ behavior {
//@ requires assigned(a, pre) /\ amt >= 0;
//@ modifies a^.credit;
//@ ensures if a^.credit^ >= amt
//@ then a'.credit' = a^.credit - amt
//@ else unchanged(a^.credit);
//@ }
Formally, the meaning of unchanged(store-ref-list)
is given as follows.
A set of type-tagged objects, UTTOs(store-ref-list),
is obtained from the store-ref-list
exactly as described above for the modifies-clause
(see section 6.2.3 The Modifies Clause).
Then unchanged(store-ref-list)
denotes the conjunction,
for each type-tagged object tto in UTTOs(store-ref-list),
of terms of the following form
(where tto.type_tag represents the LSL sort Loc[T]).
~isModified(narrow(tto.obj):Loc[T], pre, post)
In the above predicate, the trait function narrow
converts an untyped object (the result of tto.obj)
to a typed object of the type given by the type tag recorded in tto.
The sort suffix (:Loc[T]) is included to say what overloading
of narrow is desired, namely the one of from the trait
TypedObj(Loc, T), where Loc, and T are from
the type tag recorded in tto.
This is one reason why type-tagged objects are needed,
as modification is a concept defined by the notion of equality
for each kind of abstract value.
For example, the postcondition of withdraw as specified above
means the following.
if a^.credit^ >= amt
then a'.credit' = a^.credit - amt
else ~isModified(narrow(
asTypeTaggedObject(eval(a,pre).credit).obj):Obj[Money],
pre, post)
This can be simplified to the following, using the fact that widening and narrowing a typed object results in the same typed object.
if a^.credit^ >= amt then a'.credit' = a^.credit - amt else ~isModified(eval(a,pre).credit, pre, post)
(The advantage of the more complex formal semantics is that it works in more general situations.)
An lcpp-primary starting with unchanged has sort Bool.
See section 6.2.3 The Modifies Clause for the rules for the sorts allowed for
a store-ref.
See section 6.10 Case Analysis for another example of unchanged.
Go to the first, previous, next, last section, table of contents.