// @(#)$Id: default_constructor.lh,v 1.3 1998/08/27 22:56:49 leavens Exp $
#include "default_interfaces.lh"

T::T() throw();
//@ behavior {
//@   constructs self;
//@   ensures true;
//@   ensures redundantly assigned(self, post) /\ assigned(self', post); 
//@ }

[Index]

HTML generated using lcpp2html.