% @(#)$Id: State_Basics.proof,v 1.3 1998/03/26 18:58:46 leavens Exp $ set script State_Basics set log State_Basics %%% Proof Obligations for trait State_Basics execute State_Basics_Axioms %% Implications declare variables obj: Object obj1: Object st: State v: Value typs: Set[TYPE] v1: Value typs1: Set[TYPE] .. % main trait: State_Basics set name State_BasicsTheorem set box-checking on prove (emptyState ~= bottom) .. resume by contradiction <> contradiction subgoal [] contradiction subgoal [] conjecture qed prove (isBottom(st)) = (st = bottom) .. res by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal <> induction subgoal res by case stc = bottom <> case stc = bottom [] case stc = bottom <> case ~(stc = bottom) res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case ~(stc = bottom) [] induction subgoal [] conjecture qed prove (~ isBottom(st) => bind(st, obj, v, typs) ~= bottom) .. [] conjecture qed prove (~ isBottom(st) => eval(obj1, bind(st, obj1, v, typs)) = v) .. instantiate obj by obj1 in State_Basics.6 [] conjecture qed prove (~ isBottom(st) => eval(obj1, bind(st, obj, v, typs)) = (if obj1 = obj then eval(obj1, bind(emptyState, obj1, v, typs)) else eval(obj1, st))) .. res by => <> => subgoal res by case obj1 = obj <> case obj1c = objc p eval(objc, bind(stc, objc, v, typs))=v res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case obj1c = objc <> case ~(obj1c = objc) res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case ~(obj1c = objc) [] => subgoal [] conjecture qed prove (~ isBottom(st) => allocated(obj1, bind(st, obj, v, typs)) = (if obj1 = obj then allocated(obj1, bind(emptyState, obj1, v, typs)) else allocated(obj1, st))) .. res by => <> => subgoal [] => subgoal [] conjecture qed prove (bind(bind(st, obj, v, typs), obj, v1, typs1)) = (bind(st, obj, v1, typs1)) .. prove eval(obj1,bind(bind(st, obj, v, typs), obj, v1, typs1)) =eval(obj1,bind(st, obj, v1, typs1)) .. declare variables v2: Value typs2: Set[TYPE] ins st by bind(st, obj, v2, typs2) in State_Basics.6 res by case st~=bottom <> case stc ~= bottom res by case obj1 = obj <> case obj1c = objc p eval(objc, bind(bind(stc, objc, v, typs), objc, v1, typs1))=v1 res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case obj1c = objc <> case ~(obj1c = objc) res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case ~(obj1c = objc) [] case stc ~= bottom <> case ~(stc ~= bottom) set immu on prove bind(bottom, obj, v, typs)=bottom [] conjecture [] case ~(stc ~= bottom) [] conjecture set immu off prove allocated(obj1,bind(bind(st, obj, v, typs), obj, v1, typs1)) =allocated(obj1,bind(st, obj, v1, typs1)) .. res by case st=bottom <> case stc = bottom [] case stc = bottom <> case ~(stc = bottom) [] case ~(stc = bottom) [] conjecture apply State_Basics.2 to conjecture [] conjecture qed prove (bind(bind(st, obj, v, typs), obj1, v1, typs1)) = (if obj1 = obj then bind(st, obj1, v1, typs1) else bind(bind(st, obj1, v1, typs1), obj, v, typs)) .. declare variables obj2: Object v2: Value typs2: Set[TYPE] prove allocated(obj2,bind(bind(st, obj, v, typs), obj1, v1, typs1))=allocated(obj2,if obj1 = obj then bind(st, obj1, v1, typs1) else bind(bind(st, obj1, v1, typs1), obj, v,typs)) res by case st = bottom <> case stc = bottom res by case obj1 = obj <> case obj1c = objc [] case obj1c = objc <> case ~(obj1c = objc) [] case ~(obj1c = objc) [] case stc = bottom <> case ~(stc = bottom) res by case obj1 = obj <> case obj1c = objc [] case obj1c = objc <> case ~(obj1c = objc) [] case ~(obj1c = objc) [] case ~(stc = bottom) [] conjecture p eval(obj2,bind(bind(st, obj, v, typs), obj1, v1, typs1))=eval(obj2,(if obj1 = obj then bind(st, obj1, v1, typs1) else bind(bind(st, obj1, v1, typs1), obj, v, typs))) res by case st=bottom <> case stc = bottom set immu on prove bind(bottom, obj, v, typs)=bottom [] conjecture [] case stc = bottom <> case ~(stc = bottom) set immu off res by case obj1 = obj <> case obj1c = objc [] case obj1c = objc <> case ~(obj1c = objc) ins st by stc in State_Basics.6 res by case obj2=obj1c <> case obj2c = obj1c p eval(obj1c, bind(bind(stc, objc, v, typs), obj1c, v1, typs1))=v1 res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture ins st by bind(stc, obj1c, v1, typs1) in State_Basics.6 [] case obj2c = obj1c <> case ~(obj2c = obj1c) res by case obj2c= objc <> case obj2c = objc p eval(objc, bind(bind(stc, obj1c, v1, typs1), objc, v, typs))=v res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture ins st by bind(stc, objc, v2, typs2)in State_Basics.6 [] case obj2c = objc <> case ~(obj2c = objc) p eval(obj2c, bind(bind(stc, objc, v, typs), obj1c, v1, typs1))= eval(obj2c, bind(stc, objc, v, typs)) ins st by bind(stc, objc, v1, typs1) in State_Basics.6 [] conjecture ins st by bind(stc, obj1c, v1, typs1) in State_Basics.6 [] case ~(obj2c = objc) [] case ~(obj2c = obj1c) [] case ~(obj1c = objc) [] case ~(stc = bottom) [] conjecture p bind(bind(st, obj, v, typs), obj1, v1, typs1)=bottom <=> (if obj1 = obj then bind(st, obj1, v1, typs1) else bind(bind(st, obj1, v1, typs1), obj, v, typs))=bottom res by case obj1 = obj <> case obj1c = objc [] case obj1c = objc <> case ~(obj1c = objc) [] case ~(obj1c = objc) [] conjecture apply State_Basics.2 to conjecture [] conjecture qed %% Conversions freeze State_Basics %% converts allocated, eval, isBottom exempting \forall obj: Object eval(obj, %% bottom), eval(obj, emptyState) thaw State_Basics declare operators allocated': Object, State -> Bool , isBottom': State -> Bool , eval': Object, State -> Value .. % subtrait 0: State_Basics (allocated': Object, State -> Bool for allocated: % Object, State -> Bool, eval': Object, State -> Value for eval: Object, % State -> Value, isBottom': State -> Bool for isBottom: State -> Bool) set name State_Basics assert sort State partitioned by allocated', eval', isBottom' ;(~ allocated'(obj, emptyState)) ;(~ allocated'(obj, bottom)) ;(allocated'(obj, bind(st, obj1, v, typs))) = (~ isBottom'(st) /\ (obj = obj1 \/ allocated'(obj, st))) ;(~ isBottom'(st) => eval'(obj1, bind(st, obj, v, typs)) = (if obj1 = obj then v else eval'(obj1, st))) ;(~ isBottom'(emptyState)) ;(isBottom'(bottom)) ;(isBottom'(bind(st, obj, v, typs))) = (isBottom'(st)) .. declare variables obj: Object _x1_: Object _x1_: State _x2_: State .. set name exemptions assert eval(obj, bottom) = eval'(obj, bottom); eval(obj, emptyState) = eval'(obj, emptyState) .. set name conversionChecks prove (isBottom'(st)) = (st = bottom) .. res by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal <> induction subgoal [] induction subgoal [] conjecture qed prove (allocated(_x1_:Object, _x2_)) = (allocated'(_x1_:Object, _x2_)) res by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal <> induction subgoal [] induction subgoal [] conjecture qed prove (allocated(_x1_:Object, _x2_)) = (allocated'(_x1_:Object, _x2_)) [] conjecture qed prove (eval(_x1_:Object, _x2_)) = (eval'(_x1_:Object, _x2_)) res by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal <> induction subgoal res by case _x2_c=bottom <> case _x2_c = bottom set immu on p bind(bottom, o, v, s2)=bottom [] conjecture [] case _x2_c = bottom <> case ~(_x2_c = bottom) res by case _x1_=o <> case _x1_c = oc p eval(oc, bind(_x2_c, oc, v, s2))=v res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture res by con <> contradiction subgoal crit **Hyp with * [] contradiction subgoal [] case _x1_c = oc <> case ~(_x1_c = oc) p eval(_x1_c, bind(_x2_c, oc, v, s2))=eval(_x1_c,_x2_c) res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] conjecture res by con <> contradiction subgoal crit *Hyp with * [] contradiction subgoal [] case ~(_x1_c = oc) [] case ~(_x2_c = bottom) [] induction subgoal [] conjecture qed prove (eval(_x1_:Object, _x2_)) = (eval'(_x1_:Object, _x2_)) [] conjecture qed prove (isBottom(_x1_:State)) = (isBottom'(_x1_:State)) [] conjecture qed