// @(#)$Id: abstract-init.lh,v 1.1 1997/01/10 23:29:38 leavens Exp $ #include "IntHeap.lh" IntHeap myHeap; //@ behavior { ensures myHeap' = add(3, add(4, empty)); }
[Index]
HTML generated using lcpp2html.