%Please fill in the following table:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Last Name         	| 1st Name        	| Student #   	|
%			|			|		|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



a5Q1  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  
%PVS FOR Question 1 b goes here
% Put your definition of f(x) here




% Put you definition of h(x,y) here




  END a5Q1




a5Q2  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

n:VAR nat

% PVS for Huth+Ryan p. 56 #3.  
sum2(n): RECURSIVE nat =
  (IF n = 0 THEN 0 ELSE n^2 + sum2(n - 1) ENDIF)
  MEASURE id

Q2bi: THEOREM sum2(n) = (n * (n + 1)*(2*n+1))/6

Q2bii: THEOREM n>=4 IMPLIES 2^n>= n+10
  END a5Q2


% PVS for question 3 follows

sentrip % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  k_PressSP: int = 2450; k_deadBand: int = 50
  KDB:int = k_deadBand;  KHPSP:int = k_PressSP

  Trip:TYPE = {Tripped, NotTripped}

  AItype:TYPE = real

  f_PressTrip(Pressure:real,f_PressTripS1:Trip):Trip = TABLE
  | Pressure<k_PressSP-k_deadBand                  | NotTripped  ||
  | k_PressSP-k_deadBand<=Pressure&Pressure<k_PressSP|f_PressTripS1||
  | Pressure>=k_PressSP                             |Tripped      ||
  ENDTABLE

  PTRIP(PRES:AItype,PREV:bool):bool = TABLE
  |[PRES<KHPSP-KDB|KHPSP-KDB<=PRES & PRES<KHPSP|PRES>=KHPSP]|
  | FALSE           | PREV                       | TRUE     ||
  ENDTABLE


% Abstraction Functions
  Trip2bool(TripVal:Trip):bool = TABLE
  |[TripVal=Tripped|TripVal=NotTripped]|
  |  TRUE          |  FALSE           ||
  ENDTABLE

  real2AItype(x:real):AItype = x%floor(x)


% Prove this for Question 3 a

  Sentrip1:THEOREM
  (FORALL (Pressure:real,f_PressTripS1:Trip):
  Trip2bool(f_PressTrip(Pressure,f_PressTripS1)) =
    PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1)))


% Additional Definitions for status output

% Specification
  f_PressStatus(f_PressTrip:Trip,f_PressStatusS1,Transmit:bool):bool =
  TABLE
  | f_PressTrip=Tripped                    | TRUE           ||
  | NOT(f_PressTrip=Tripped)&Transmit      | FALSE          ||
  | NOT(f_PressTrip=Tripped)& NOT Transmit | f_PressStatusS1||
  ENDTABLE

% Implementation
  STATUS(PRES:AItype,PREV:bool):bool = TABLE
  |[PRES<KHPSP-KDB|KHPSP-KDB<=PRES & PRES<KHPSP|PRES>=KHPSP]|
  | PREV         | PREV                       | TRUE     ||
  ENDTABLE




% Try this for Question 3 b

  Status1:THEOREM
  (FORALL (Pressure:real,f_PressTripS1:Trip,f_PressStatusS1,Transmit:bool):
  f_PressStatus(f_PressTrip(Pressure,f_PressTripS1),f_PressStatusS1,Transmit) =
    IF NOT(Transmit) THEN STATUS(real2AItype(Pressure),f_PressStatusS1)
    ELSE FALSE %PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1))
    ENDIF)

% for Question 3 f state & prove theorem Status2 here





% for Question 3 h add new definitions and prove theorem Status3 here




  END sentrip