-- (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: pocall.d
-- Author: Rob Strom
-- SCCS Info: @(#)pocall.d	1.2 3/13/90

-- definitions used by pocall
pocall: USING(InferredType, tscheck) 
definitions
-- procedure to compute an adds/drops given a pre-condition/post-condition pair
GetAddsDropsCall: CALLMESSAGE (
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  InferredDcls: InferredDefinitions, -- declarations inferred by typechecking
  Definitions: Definitions_Modules, -- definitions used by program
  Operands: Objectnames, -- the operand list of the CALL statement
  CallmessageComponents: Component_Declarations, -- from the definition of the callmessage type
  Precondition: Formal_Typestate, -- the entry typestate
  Postcondition: Formal_Typestate, -- the exit typestate
  AddDropSet: AddDropSet -- the add and drop set
)
CONSTANT(Services, Declarations, InferredDcls, Definitions, Operands, CallmessageComponents, Precondition, Postcondition)
EXIT{full};
GetAddsDropsInport: INPORT OF GetAddsDropsCall {Full(Services), full(Declarations), full(InferredDcls), full(Definitions), full(Operands), full(CallmessageComponents), full(Precondition), full(Postcondition)};
GetAddsDropsOutport: OUTPORT OF GetAddsDropsInport;

end definitions
