tripmeter[ LO: real, % low trip threshold HI: { x: real | x > LO }, % high trip threshold D: { x: real | % the amount of hysteresis x >= 0 AND HI - x >= LO + x } ]: THEORY BEGIN IMPORTING machine %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % General tip: don't hesitate to try out the automated tactics of PVS % notably (grind) and (induct-and-simplify). These should make easy % work of most of the lemmas, until you get to exercise 2.7 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % An implementation of the tripmeter using a 3-element enumeration % as state %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% state2: TYPE+ = {Ht, Lt, Ut} % enumeration type with three elements delta2 : [state2,real->state2] = LAMBDA (s2: state2, x: real): COND x > HI OR (s2 = Ht AND x > HI - D) -> Ht, x < LO OR (s2 = Lt AND x < LO + D) -> Lt, ELSE -> Ut ENDCOND tm2: machine[state2, real, bool] = (# delta := delta2, output:= LAMBDA (s2: state2): s2 /= Ut #) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % An alternative definition of transition function for state2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% delta22 : [state2,real->state2] = LAMBDA (s2: state2, x: real): COND x > HI -> Ht, s2 = Ht AND HI-D < x AND x <= HI -> Ht, x < LO -> Lt, s2 = Lt AND LO <= x AND x < LO+D -> Lt, ELSE -> Ut ENDCOND tm22: machine[state2, real, bool] = (# delta := delta22, output:= LAMBDA (s2: state2): s2 /= Ut #) IMPORTING machine_equiv[state2,state2,real,bool] % EXERCISE 2.1 % Prove the two lemmas below tm2_refines_tm22: LEMMA trace_refines(tm2, (LAMBDA(x:state2):x), tm22) tm22_refines_tm2: LEMMA trace_refines(tm22, (LAMBDA(x:state2):x), tm2) % EXERCISE 2.2 % Prove the lemma below. % You may have to use (apply-extensionality) equal_delta2_and_delta22: LEMMA delta2 = delta22 % Note that given lemma equal_delta2_and_delta22 above % it's rather obvious that tm2 and tm22 refine each other, % as in fact tm2 and tm22 are the same machine. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Now an implementation using 2 booleans as state %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% state1: TYPE+ = [# LT, HT: bool #] s1: VAR state1 x: VAR real % EXERCISE 2.3 % Correct the definition of tm1 below % (The definition given below is WRONG and just illustrates the syntax) tm1: machine[state1, real, bool] = (# delta := LAMBDA (s1: state1, x: real): (# LT := x < LO, HT := x > HI #), output:= LAMBDA (s1: state1): HT(s1) OR LT(s1) #) % EXERCISE 2.4 % Prove the lemma below, which states that tm1 will never % end up in the state where both LT and HT are true. never_in_TRUE_TRUE : LEMMA (FORALL (s1:state1, inp:sequence[real], n:nat) : s1 /= (# LT := TRUE, HT := TRUE #) => trace(tm1)(s1,inp)(n) /= (# LT := TRUE, HT := TRUE #)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % tm2 refines tm1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% IMPORTING machine_equiv[state2,state1,real,bool] % EXERCISE 2.5 % Define a suitable function rho and prove the two lemmas below % (The definition of rho below is WRONG and just illustrates % the syntax) rho(s2: state2): state1 = COND Lt = s2 -> (# LT := FALSE, HT := FALSE #), Ht = s2 -> (# LT := FALSE, HT := FALSE #), Ut = s2 -> (# LT := FALSE, HT := FALSE #) ENDCOND tm2_trace_refines_tm1: LEMMA trace_refines(tm2, rho, tm1) tm2_output_refines_tm1: LEMMA output_refines(tm2, rho, tm1) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Below some more properties of tm2, which try to give a logical % characterisation of its behaviour %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % EXERCISE 2.6 % Prove the lemma below, which says what the last input % of tm2 must have been if it is in state Ht. tm2_becomes_Ht : LEMMA (FORALL (inp_seq:sequence[real],n:nat) : trace(tm2)(Ut,inp_seq)(n+1) = Ht IMPLIES (trace(tm2)(Ut,inp_seq)(n) = Ht AND HI-D < inp_seq(n+1) AND inp_seq(n+1) <= HI ) OR inp_seq(n+1) > HI ) % EXERCISE 2.7 % Prove the lemma below % NB (grind) won't work; you'll have to supply clever % instantiations of the existential quantifications by hand. % To use lemma tm2_becomes_Ht, give the command % (lemma "tm2_becomes_Ht") Ht_implies_too_high : LEMMA (FORALL (inp_seq:sequence[real]) : FORALL (n:nat) : trace(tm2)(Ut,inp_seq)(n) = Ht IMPLIES (EXISTS (too_hi:nat) : 0 < too_hi AND too_hi <= n AND inp_seq(too_hi) > HI AND (FORALL (j:nat) : too_hi (HI-D < inp_seq(j) AND inp_seq(j) <= HI) ) ) ) % EXERCISE 2.8 % Write and prove similar lemmas to the two lemmas above, % but now for state Ut instead of Ht. % EXERCISE 2.9 % Now prove the lemma below, giving the reverse implication % to Ht_implies_too_high too_high_implies_Ht: LEMMA (FORALL (inp_seq:sequence[real]) : FORALL (n:nat) : (EXISTS (too_hi:nat) : 0 < too_hi AND too_hi <= n AND inp_seq(too_hi) > HI AND (FORALL (j:nat) : too_hi (HI-D < inp_seq(j) AND inp_seq(j) <= HI) ) ) IMPLIES trace(tm2)(Ut,inp_seq)(n) = Ht ) % EXERCISE 2.10 % Write and prove a similar lemma for Lt, ie a lemma % too_low_implies_Lt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A more abstract machine, which uses a list of reals as state. % % This machine is more like a specification; unlike the machines above, % it does not provide an executable implementation . %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% l : VAR list[real] delta3 (l,x) : list[real] = cons(x,l) output3 (l) : bool = (EXISTS (i:nat) : i < length(l) AND nth(l,i) > HI AND FORALL (j:nat) : j (HI-D < nth(l,j) AND nth(l,j) <= HI)) OR (EXISTS (i:nat) : i < length(l) AND nth(l,i) < LO AND FORALL (j:nat) : j ( LO < nth(l,j) AND nth(l,j) <= LO+D)) tm3: machine[list[real], real, bool] = (# delta := delta3, output:= output3 #) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % tm3 refines tm2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% rho3(l) : state2 = IF (EXISTS (i:nat) : i < length(l) AND nth(l,i) > HI AND FORALL (j:nat) : j (HI-D < nth(l,j) AND nth(l,j) <= HI)) THEN Ht ELSE IF (EXISTS (i:nat) : i < length(l) AND nth(l,i) < LO AND FORALL (j:nat) : j ( LO < nth(l,j) AND nth(l,j) <= LO+D)) THEN Lt ELSE Ut ENDIF ENDIF IMPORTING machine_equiv[list[real],state2,real,bool] tm3_output_refines_tm2: LEMMA output_refines(tm3, rho3, tm2) END tripmeter