// @(#)$Id: ApplyTwice.lh,v 1.15 1998/09/23 16:02:18 ruby Exp $

typedef int (*int_fun)(int) throw();

extern int ApplyTwice(int_fun f, int i
                     /*@ expects NoSideEffectsDetFun(int, int) @*/) throw();
//@ behavior {
//@   requires assigned(f, pre)
//@            /\ (*f)^ satisfies
//@                       int ignored(int j) throw()
//@                       behavior {
//@                         requires inDomain(j);
//@                         ensures result = resultFor(j) /\ inRange(result);
//@                       }
//@            /\ inDomain(i) /\ inDomain(resultFor(j));
//@   ensures result = resultFor(resultFor(j));
//@   ensures redundantly inRange(result);
//@   example \forall j: int (inDomain(j)
//@                           => (between(0, j, 30) /\ resultFor(j) = j+1))
//@           /\ i = 5 /\ result = 7;
//@ }

[Index]

HTML generated using lcpp2html.