% @(#)$Id: AllocatedAssigned.proof,v 1.2 1997/02/13 00:21:07 leavens Exp $ set script AllocatedAssigned set log AllocatedAssigned %%% Proof Obligations for trait AllocatedAssigned execute AllocatedAssigned_Axioms %% Implications declare variables loc: Loc[T] st: State .. % main trait: AllocatedAssigned set name AllocatedAssignedTheorem prove (allocated(loc, st) => widen(loc) \in domain(st)) by => .. <> => subgoal [] => subgoal [] conjecture qed prove (assigned(loc, st) => allocated(loc, st)) by => .. <> => subgoal [] => subgoal [] conjecture qed %% Conversions freeze AllocatedAssigned %% converts assigned, allocated: Loc[T], State -> Bool thaw AllocatedAssigned declare operators allocated': Loc[T], State -> Bool , assigned': Loc[T], State -> Bool .. % subtrait 0: AllocatedAssigned (assigned': Loc[T], State -> Bool for % assigned: Loc[T], State -> Bool, allocated': Loc[T], State -> Bool for % allocated: Loc[T], State -> Bool) set name AllocatedAssigned assert (allocated'(loc, st)) = (allocated(widen(loc), st) /\ type_of(loc) \in types_of(widen(loc), st)) ;(assigned'(loc, st)) = (allocated'(loc, st) /\ narrow(eval(widen(loc), st)) ~= unassigned) .. % subtrait 0.5: SortNames (Loc[T] for S, TYPE for SORTNAME, type_of: Loc[T] -> % TYPE for sort_of: S -> SORTNAME) % with renaming (Loc[T] for S, TYPE for SORTNAME, type_of: Loc[T] -> TYPE % for sort_of: S -> SORTNAME) % subtrait 0.1: State % subtrait 0.1.1: State_Basics % subtrait 0.1.2: TypePerspectives % subtrait 0.1.2.2: Set (TYPE for E, Set[TYPE] for C, int for Int) % subtrait 0.1.2.2.1: SetBasics % with renaming (TYPE for E, Set[TYPE] for C) % subtrait 0.1.2.2.2: Integer % with renaming (int for Int) % subtrait 0.1.2.2.2.1: DecimalLiterals (Int for N) % with renaming (int for N) % subtrait 0.1.2.2.2.2: TotalOrder (Int for T) % with renaming (int for T) % subtrait 0.1.2.2.2.2.1: IsTO % with renaming (int for T) % subtrait 0.1.2.2.2.2.2: DerivedOrders % with renaming (int for T) % subtrait 0.1.2.2.3: DerivedOrders (C for T, __ \subseteq __: C, C -> Bool % for __ <= __: T, T -> Bool, __ \supseteq __: C, C -> Bool for __ >= __: T, % T -> Bool, __ \subset __: C, C -> Bool for __ < __: T, T -> Bool, __ % \supset __: C, C -> Bool for __ > __: T, T -> Bool) % with renaming (Set[TYPE] for T, __ \subseteq __: Set[TYPE], Set[TYPE] -> % Bool for __ <= __: T, T -> Bool, __ \supseteq __: Set[TYPE], Set[TYPE] % -> Bool for __ >= __: T, T -> Bool, __ \subset __: Set[TYPE], Set[TYPE] % -> Bool for __ < __: T, T -> Bool, __ \supset __: Set[TYPE], Set[TYPE] % -> Bool for __ > __: T, T -> Bool) % subtrait 0.1.3: State_Updates % subtrait 0.1.4: StateDeprecated % subtrait 0.1.4.3: UntypedFreshSemantics % subtrait 0.1.5: Set (Object for E, Set[Object] for C, int for Int) % subtrait 0.1.5.1: SetBasics % with renaming (Object for E, Set[Object] for C) % subtrait 0.1.5.2: Integer % with renaming (int for Int) % duplicate of subtrait 2.2.2: Integer % subtrait 0.1.5.3: DerivedOrders (C for T, __ \subseteq __: C, C -> Bool for % __ <= __: T, T -> Bool, __ \supseteq __: C, C -> Bool for __ >= __: T, T % -> Bool, __ \subset __: C, C -> Bool for __ < __: T, T -> Bool, __ \supset % __: C, C -> Bool for __ > __: T, T -> Bool) % with renaming (Set[Object] for T, __ \subseteq __: Set[Object], % Set[Object] -> Bool for __ <= __: T, T -> Bool, __ \supseteq __: % Set[Object], Set[Object] -> Bool for __ >= __: T, T -> Bool, __ \subset % __: Set[Object], Set[Object] -> Bool for __ < __: T, T -> Bool, __ % \supset __: Set[Object], Set[Object] -> Bool for __ > __: T, T -> Bool) % subtrait 0.2: WithUnassigned (T for T, WithUnassigned[T] for % WithUnassigned[T]) % subtrait 0.3: WidenNarrow (Loc[T] for Typed, Object for Untyped) % subtrait 0.4: WidenNarrow (WithUnassigned[T] for Typed, Value for Untyped) declare variables _x1_: Loc[T] _x2_: State .. set name conversionChecks prove (assigned(_x1_, _x2_)) = (assigned'(_x1_, _x2_)) [] conjecture qed prove (assigned(_x1_, _x2_)) = (assigned'(_x1_, _x2_)) [] conjecture qed prove (allocated(_x1_, _x2_)) = (allocated'(_x1_, _x2_)) [] conjecture qed prove (allocated(_x1_, _x2_)) = (allocated'(_x1_, _x2_)) [] conjecture qed