A5_02_Q2 : THEORY

  BEGIN
  x,y:VAR real

  % Improve the definition of f(x) by refining the return type

  f(x):real = x^2+4*x-5
 

  ln(x:posreal):real

  % Make best definition of g(x,y) that eliminates unprovable TCCs
  g(x,y):real = ln(x-y^2)

  END A5_02_Q2




A5_02_Q4 : THEORY

  BEGIN

  A:type+
x,y:VAR A

C1(x,y):bool
C2(x,y):bool
C3(x,y):bool
f1(x,y):A
f2(x,y):A
f3(x,y):A

 f(x,y): A =   TABLE  
                %-----------------------------% 
                |[ C1(x,y)|C2(x,y) |C3(x,y) ]|
                %-----------------------------%
                |  f1(x,y)   | f2(x,y)|f3(x,y)||
                %-------------------------------% 
                ENDTABLE 
  END A5_02_Q4


a5_02_Q4b  : THEORY
 BEGIN

 x: VAR real
                      %--------------% 
 f1(x): real = TABLE  |[ x<0 | x>=0 ]|
                      %--------------%
                      |  x   | 2*x  ||
             ENDTABLE %--------------%

                      %---------------%
 f2(x): real = TABLE  |[ x<=0 | x>=0 ]|
                      %---------------%
                      |   x   | 2*x  ||
             ENDTABLE %---------------%

 same: THEOREM FORALL (x:real): f1(x)=f2(x)    

  END a5_02_Q4b


prog_ver : THEORY
  BEGIN

  n: int
  i: VAR nat
  AType: TYPE+
  key: VAR AType

  A(i:{k:nat|k<=n-1}):AType

  V(i,key):bool = (0<= n)
  B(i,key):bool = (0<=i) & (i<=n) & (A(i)/=key)
  I(i,key):bool = (0<=i) & (i<=n) & (forall (j:{k:nat|k<=i-1}): A(j)/=key)
  P(i,key):bool = (0<=i) & (i<=n) &  (forall (j:{k:nat|k<=i-1}): A(j)/=key)
                   & (i=n OR A(i)=key)

  C1: THEOREM V(i,key) => I(0,key)
  C2: THEOREM I(i,key)& B(i,key) => I(i+1,key)
  C3: THEOREM I(i,key)& NOT B(i,key) => P(i,key)

  END prog_ver