-- (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. 
-- SCCS Info: @(#)typestate_inference.d	1.1 4/3/89

typestate_inference: using (predefined)
definitions

-- Typestate precondition rules:
Precondition_Rules: ORDERED TABLE OF Precondition_Rule {full};
Precondition_Rule: RECORD (
  Precondition_Function: Precondition_Function_Name, -- Function to compute Required, Forbidden, Vars, and Pos
  Affected_Operands: Operand_Offsets -- which operands to look at
);

Precondition_Function_Name: ENUMERATION ('init', 'var', 'pos', 'assertable', 'callpreconditions', 'full', 'checked', 'casets', 'lowestelementstate', 'lowestpostcondition', 'initwithoutcase', 'lowestentrycondition', 'polymorphprecondition', 'rangeerror?', 'uncopyable?', 'duplicatekey?');

Operand_Offsets: ORDERED TABLE OF integer {full};

PostconditionRuleFormat: ENUMERATION('regular', 'call', 'exit', 'compound');

-- Typestate Postcondition rules:
-- Operations which are themselves control constructs don't have postcondition rules
Postcondition: VARIANT OF PostconditionRuleFormat (
  'regular' -> RegularRule: RegularPostconditionInfo  {full},
  'call' -> Call: empty {},
  'exit' -> Exit: empty {},
  'compound' -> Compound: empty {});
 
RegularPostconditionInfo: RECORD (
  Rule: PostconditionRuleElements,
  Exceptions:  Exceptions);
  
PostconditionRuleElements: ORDERED TABLE OF PostconditionRuleElement {full};

Exceptions: TABLE OF Builtin_Exception {full} keys(*);

PostconditionRuleElement: RECORD (
  PostconditionFunction: PostconditionFunctionName, -- Function to compute Adds and Drops
  AffectedOperands: Operand_Offsets -- which operands to look at
);

PostconditionFunctionName: ENUMERATION ('makeinit', 'asserted', 'makechecked', 'copy', 'makeuninit', 'movets', 'killvariant', 'dropcomponents', 'killconstraints', 'moveentryts', 'moveelementts', 'makecase', 'polymorphts', 'makefull');

end definitions
