Go to the first, previous, next, last section, table of contents.

6.3.1 Fresh

A lcpp-primary beginning with fresh, for example fresh(x), can only be used in a postcondition. (See section 6.1.10 Larch/C++ Special Primaries for the exact syntax.) Informally, fresh(x) says that the object denoted by the term x was not allocated in the pre-state, and is allocated in the post-state. Writing fresh(t1,t2) says that both t1 and t2 are newly allocated, and that, in addition, t1 and t2 are distinct objects.

A common use of fresh is to state that the result of a function call is newly allocated. For example, consider the following, which says that the result of a call to make_ratl must be a pointer to newly allocated memory. 

// @(#)$Id: make_ratl.lh,v 1.7 1997/06/03 20:30:13 leavens Exp $
typedef int *ratl;
extern ratl make_ratl(int n, int d) throw();
//@ behavior {
//@   requires d > 0;
//@   ensures assigned(result, post) /\ size(locs(result)) = 2
//@           /\ (result[0])' = n /\ (result[1])' = d
//@           /\ fresh(result[0], result[1]);
//@ }

The terms in the term-list passed to fresh should usually be of sort Set[TypeTaggedObject] or a sort of the form Obj[T] or ConstObj[T], for some sort T; alternatively, as a syntactic sugar, they can be terms of a sort for which the trait function contained_objects is defined. The syntactic sugar obtains a set of objects (which must not be empty) from a value by applying contained_objects to the value and the post-state.

(Since the post-state is used, the syntax of a store-ref-list is not used with fresh, because the syntactic sugar for a store-ref-list uses the pre-state.)

The semantics of fresh(term-list) is as follows. Let E be a term in the term-list. Let TTO(E) be defined as follows.

Then ignoringTypeTags(TTO(E)) is a set of untyped objects obtained from TTO(E) by taking off each type tag from each object in TTO(E). Let AssertedFresh(term-list) be the union of the sets TTO(E), for each term E in term-list. Somewhat informally, this is summarized as follows. 

AssertedFresh(term-list) = { tto | tto is in TTO(E),
                                         E is a term in term-list }

Then fresh(term-list), means that for each E in term-list, the sets ignoringTypeTags(TTO(E)) are mutually disjoint, and that the following is true, for each typed object sort Loc[T]. 

\A loc:Loc[T]
 (loc \in AssertedFresh(term-list) => isFresh(loc, pre, post))

For example, the term fresh(result[0], result[1]) used in the above example has the following meaning, because the only sort in question is Obj[int]. 

  (ignoringTypeTags({asTypeTaggedObject(result[0])})
    \I ignoringTypeTags({asTypeTaggedObject(result[1])}))
   = {}
/\ (\A loc:Obj[int]
      (loc \in ({asTypeTaggedObject(result[0])}
               \U {asTypeTaggedObject(result[1])})
       => isFresh(loc, pre, post)))

The above can be simplified, using facts about type-tagged objects, to the following. 

({widen(result[0])} \I {widen(result[1])}) = {}
/\ isFresh(result[0], pre, post) /\ isFresh(result[1], pre, post)

The trait FreshSemantics below gives the definitions of the trait function isFresh used in the semantics. (See section 6.2.3 The Modifies Clause for the trait TypeTaggedObject that defines the trait function ignoringTypeTags.) 

% @(#)$Id: FreshSemantics.lsl,v 1.10 1995/11/13 22:20:37 leavens Exp $

FreshSemantics(Loc, T): trait
  assumes AllocatedAssigned(Loc, T)
  introduces 
    isFresh: Loc[T], State, State -> Bool
  asserts
    \forall loc: Loc[T], pre, post: State
      isFresh(loc, pre, post)
        == ~allocated(loc, pre) /\ allocated(loc, post);
  implies
    converts isFresh
      exempting \forall loc: Loc[T], st:State
        isFresh(loc, bottom, st), isFresh(loc, st, bottom)

The sort of a lcpp-primary of the form fresh(t) is Bool.

In the specification of make_ratl given above, and in similar cases, it is inconvenient to have to explicitly list each element of an array pointed at as fresh. But since the trait function contained_objects is defined for pointers (see section 11.8 Pointer Types), the syntactic sugar described above allows one to write in the specification of make_ratl fresh(result) as a shorthand for fresh(result[0], result[1]). In general, when a is a pointer or an array name, then fresh(a) means the fresh(contained_objects(a,post)). This sugar works for multi-dimensional arrays as well; that is, when a is the name of a multi-dimensional array fresh(a) means that each element is fresh. (See section 11.7 Array Types for details on the trait function contained_objects for arrays).

For structs, one has to pass to fresh both the struct object itself, and the contained objects. This can be done, as in the first conjunct of the following specification's postcondition. (See section 11.10 Structure and Class Types for the abstract values of structs.) 

// @(#)$Id: make_sratl.lh,v 1.8 1997/07/31 17:25:53 leavens Exp $
struct sratl { int num; int den; };
extern sratl& make_sratl(int n, int d) throw();
//@ behavior {
//@   requires d > 0;
//@   ensures fresh(result, result'.num, result'.den)
//@           /\ assigned(result, post)
//@           /\ assigned(result.num, post) /\ assigned(result.den, post)
//@           /\ result'.num' = n /\ result'.den' = d;
//@ }

In the above specification, fresh(result, result'.num, result'.den) could also have been written as one of the two following terms. 

  fresh(result, result')
  fresh(result, contained_objects(result',post))

If u is a union object, then usually one would write fresh(u, contained_objects(u', post)) to assert that u and its fields are fresh. See section 11.11 Union Types for more details on the abstract values of unions.

Go to the first, previous, next, last section, table of contents.