% @(#)$Id: TrashesSemantics.proof,v 1.2 1997/02/13 00:21:18 leavens Exp $ set script TrashesSemantics set log TrashesSemantics %%% Proof Obligations for trait TrashesSemantics execute TrashesSemantics_Axioms %% Implications declare variables loc: Loc[T] pre: State post: State .. % main trait: TrashesSemantics set name TrashesSemanticsTheorem prove (isTrashed(loc, pre, post) => (allocated(loc, pre) /\ (~ allocated(loc, post) \/ ~ assigned(loc, post)))) by => .. <> => subgoal res by /\ <> /\ subgoal res by case ~(allocated(widen(locc), postc)/\ type_of(locc) \in types_of(widen(locc), postc)) <> case %% ~(allocated(widen(locc), postc) %% /\ type_of(locc) \in types_of(widen(locc), postc)) [] case %% ~(allocated(widen(locc), postc) %% /\ type_of(locc) \in types_of(widen(locc), postc)) <> case %% ~(~(allocated(widen(locc), postc) %% /\ type_of(locc) \in types_of(widen(locc), postc))) [] case %% ~(~(allocated(widen(locc), postc) %% /\ type_of(locc) \in types_of(widen(locc), postc))) [] /\ subgoal <> /\ subgoal res by con <> contradiction subgoal [] contradiction subgoal [] /\ subgoal <> /\ subgoal res by con <> contradiction subgoal [] contradiction subgoal [] /\ subgoal [] => subgoal [] conjecture qed prove (isTrashed(loc, pre, post) => ~ assigned(loc, post)) .. res by => <> => subgoal res by con <> contradiction subgoal [] contradiction subgoal [] => subgoal [] conjecture qed prove (~ isTrashed(loc, pre, post)) = ((~ assigned(loc, pre) \/ assigned(loc, post)) /\ (~ allocated(loc, pre) \/ allocated(loc, post))) .. res by case type_of(loc) \in types_of(widen(loc), pre) <> case type_of(locc) \in types_of(widen(locc), prec) res by case allocated(widen(locc), prec) <> case allocated(widen(locc), prec) res by case type_of(locc) \in types_of(widen(locc), post) <> case type_of(locc) \in types_of(widen(locc), postc) res by case allocated(widen(locc), postc) <> case allocated(widen(locc), postc) res by case narrow(eval(widen(locc), postc)) = unassigned <> case narrow(eval(widen(locc), postc)) = unassigned [] case narrow(eval(widen(locc), postc)) = unassigned <> case ~(narrow(eval(widen(locc), postc)) = unassigned) [] case ~(narrow(eval(widen(locc), postc)) = unassigned) [] case allocated(widen(locc), postc) <> case ~allocated(widen(locc), postc) [] case ~allocated(widen(locc), postc) [] case type_of(locc) \in types_of(widen(locc), postc) <> case ~(type_of(locc) \in types_of(widen(locc), postc)) [] case ~(type_of(locc) \in types_of(widen(locc), postc)) [] case allocated(widen(locc), prec) <> case ~allocated(widen(locc), prec) [] case ~allocated(widen(locc), prec) [] case type_of(locc) \in types_of(widen(locc), prec) <> case ~(type_of(locc) \in types_of(widen(locc), prec)) [] case ~(type_of(locc) \in types_of(widen(locc), prec)) [] conjecture qed prove ((~ isTrashed(loc, pre, post) /\ assigned(loc, pre)) => assigned(loc, post)) by => .. <> => subgoal [] => subgoal [] conjecture qed prove ((~ isTrashed(loc, pre, post) /\ allocated(loc, pre)) => allocated(loc, post)) by => .. <> => subgoal [] => subgoal [] conjecture qed %% Conversions freeze TrashesSemantics %% converts isTrashed exempting \forall loc: Loc[T], st: State isTrashed(loc, %% bottom, st), isTrashed(loc, st, bottom) thaw TrashesSemantics declare operators isTrashed': Loc[T], State, State -> Bool .. % subtrait 0: TrashesSemantics (isTrashed': Loc[T], State, State -> Bool for % isTrashed: Loc[T], State, State -> Bool) set name TrashesSemantics assert (isTrashed'(loc, pre, post)) = ((assigned(loc, pre) /\ ~ assigned(loc, post)) \/ (allocated(loc, pre) /\ ~ allocated(loc, post))) .. % 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: AllocatedAssigned (Loc for Loc, T for T, WithUnassigned[T] for % WithUnassigned[T], Loc[T] for Loc[T]) % subtrait 0.2.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.2.1: State % duplicate of subtrait 1: State declare variables loc: Loc[T] st: State _x1_: Loc[T] _x2_: State _x3_: State .. set name exemptions assert isTrashed(loc, bottom, st) = isTrashed'(loc, bottom, st); isTrashed(loc, st, bottom) = isTrashed'(loc, st, bottom) .. set name conversionChecks prove (isTrashed(_x1_, _x2_, _x3_)) = (isTrashed'(_x1_, _x2_, _x3_)) [] conjecture qed prove (isTrashed(_x1_, _x2_, _x3_)) = (isTrashed'(_x1_, _x2_, _x3_)) [] conjecture qed prove (isTrashed(_x1_, _x2_, _x3_)) = (isTrashed'(_x1_, _x2_, _x3_)) [] conjecture qed