-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- File: pomakefull.d
-- Author: Rob Strom
-- SCCS Info: @(#)pocall.d	1.1 7/27/89

-- definitions used by pocall
pomakefull: USING(tscheck) 
definitions
RecursivePostconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate checking environment
  Definitions: Definitions_Modules, -- definitions used by program
  Source: ObjectName, -- object being recursively processed
  CurrentTS: Typestate, -- typestate at point where statement is executed
  NormalPostcondition: AddDropSet -- changes to TS for normal outcome
)
CONSTANT(Services, Declarations, Context, Definitions, CurrentTS)
EXIT{full} MINIMUM{full}
;
RecursivePostconditionInport: INPORT OF RecursivePostconditionCall {Full};
RecursivePostconditionOutport: OUTPORT OF RecursivePostconditionInport;

end definitions
