-- (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: typestate.d
-- Author: Rob Strom
-- SCCS Info: @(#)typestate.d	1.1 7/27/89

-- interface from root program to typestate checker

typestate: USING (stdenv, coercions, checking_table, inferredtype, errors)

DEFINITIONS

TypestateCheckCall: CALLMESSAGE(
  StdEnv: StdEnv, -- standard external environment
  Program: program, -- program being checked
  proc: proc, -- process in program
  Checking_Table: Checking_Table, -- set of rules
  DefinitionsMaps: Definitions_PrintMappings, -- printmappings for defs
  ExecutableMap: Executable_PrintMappings, -- printmappings for executable
  InferredDefinitions: InferredDefinitions, -- definitions inserted by typechecking
  Coercions: Coercions, -- coercions inserted by typestate checking
  ErrorMessages: Errors -- error messages 
) CONSTANT(Program,Proc, StdEnv, Checking_Table, DefinitionsMaps, ExecutableMap, InferredDefinitions) EXIT{full}
  MINIMUM {full(StdEnv), full(Program), /* Checked(Program), */  full(proc), full(Checking_table),
  full(DefinitionsMaps), full(ExecutableMap), full(InferredDefinitions)}
  EXCEPTION TypestateErrors {full(StdEnv), full(Program), /* Checked(Program), */ full(proc), full(Checking_table), full(DefinitionsMaps), full(ExecutableMap), full(InferredDefinitions), full(ErrorMessages)}
;

TypestateCheckInport: INPORT OF TypestateCheckCall
  {full(StdEnv), full(Program), /* Checked(Program), */ full(Proc), full(Checking_table), 
  full(DefinitionsMaps), full(ExecutableMap), full(InferredDefinitions)};
  
TypestateCheckOutport: OUTPORT OF TypestateCheckInport;
  
END DEFINITIONS
