======================================================================== 
		   Problems for the Examination of
     the Sinaia School on Formal Verification of Software Systems
			   03-10 March 2008

======================================================================== 
			    Instructions
======================================================================== 

0. Deadline: April 30 (Wed), 2008

1. Send your answers via e-mail:
    - The subject of the mail should be "Sinaia School Exam".
    - USE CARBON COPY or COPY facility of e-mail system and KEEP A
      COPY AT YOUR HAND.  The copy should be an evidence of your
      submission, if your mail is lost in delivery.

  The header of your mail should be as follows:

     To: kokichi@jaist.ac.jp,
         ogata@jaist.ac.jp,
         masaki-n@jaist.ac.jp,
     Cc: <your-mail-address>
     Subject: Sinaia School Exam

2. Write your report in plain text. Prepare separate files for
   different questions which requires codes (specs and/or proof
   scores) in CafeOBJ.

3. Advices in writing your answers for Problems 3-2,3-4,4-1,4-2 and 5:

   For the problems which require CafeOBJ specs and/or proof scores,
   the answer should be composed of the following three items: (1)
   Specifications, (2) Proof score (with enough comments to understand
   your proof), (3) Outputs of CafeOBJ system for the specifications
   and/or the proof scores.  The outputs can be shortened if they are
   long, but make it sure that they are certainly processed by CafeOBJ
   system properly.

   The followings show an example style of short files containing
   CafeOBJ codes. Please prepare different files for different
   questions for making it easy to check your answers by CafeOBJ
   system.

   ====================================================================
   -- ************************************
   -- beginning of your specification.
   mod! BASIC-INT{.....}

   ..

   -- ************************************
   -- beginning of your proof score.
   open INT+
   --> Proof of the commutativity and the associativity of _+_ .
   .
   --> Lemma 1: xxxxx = yyyyy for any integer I.
   --> Induction step
   close


   -- The CafeOBJ system terminates to read this file, here.
   eof

   -- ******************************
   -- begin of your outputs.
   CafeOBJ> in <yourReport>.mod
   processing input : ./<yourReport>.mod
   -- defining module! BASIC-INT.......__*** done.
   ..
   -- opening module BASIC-INT.. done._*
   -- reduce in %BASIC-INT : 0 + j = j + 0
   true : Bool
   (0.000 sec for parse, 3 rewrites(0.000 sec), 5 matches)
   ..
   ====================================================================

   For more longer answers, follow the file structure of ABP case
   study (the structure of accompanying CafeOBJ files of the Lecture
   Note 7).

=======================================================================
			      Problem 1
=======================================================================
Let CafeOBJ modules BASIC-NAT, NATf1 and NATf2 be defined as follows:

mod! BASIC-NAT {
  [Nat]
  op 0 : -> Nat 
  op s_ : Nat -> Nat 
}

mod* NATf1 { 
 pr(BASIC-NAT)
 op f1 : Nat -> Nat
 var N : Nat
 eq f1(N) = (s s 0) .
}

mod* NATf2 { 
 pr(BASIC-NAT)
 op f2 : Nat -> Nat
 op n : -> Nat 
 eq f2(n) = (s s 0) .
}

(1.1) Describe the models of NATf1.  That is, explain the models which
      satisfies the specification NATf1.  Which model of NATf1
      satisfies the equation "eq f1(s 0) = (s s 0) ."?.

(1.1) Describe the models of NATf2.  That is, explain the models which
      satisfies the specification NATf2.  Which model of NATf2
      satisfies the equation "eq f2(s 0) = (s s 0) ."?.

=======================================================================
			      Problem 2
=======================================================================
The built-in BOOL module of CafeOBJ contains the following signature
and equations.  Try to check this by using "show BOOL" in CafeOBJ
system.  Notice that the predicates (_ and-also _) and (_ or-else _)
are omitted.  Answer the following two problems of (2-1) and (2-2).

-- ---------------------------------------------
-- Signature of BOOL ---------------------------
-- ---------------------------------------------
[ Bool ]
-- ---------------------------------------------
-- two constants
ops true false : -> Bool
-- two constructors
op _ and _ : Bool Bool -> Bool 
             { assoc comm prec: 55 r-assoc }
op _ xor _ : Bool Bool -> Bool 
             { assoc comm prec: 57 r-assoc }
-- ---------------------------------------------
op _ or _ : Bool Bool -> Bool 
             { assoc comm prec: 59 r-assoc }
op not _ : Bool -> Bool 
             { strat: (0 1) prec: 53 }
op _ implies _ : Bool Bool -> Bool 
             { strat: (0 1 2) prec: 61 r-assoc }
op _ iff _ : Bool Bool -> Bool 
             { strat: (0 1 2) prec: 63 r-assoc }
-- ---------------------------------------------
--
-- ---------------------------------------------
-- Equations of BOOL ---------------------------
-- ---------------------------------------------
var A : Bool
var B : Bool
var C : Bool
-- _and_
eq false and A     = false .
eq true  and A     = A .
eq     A and A     = A .
eq A and (B xor C) = (A and B) xor (A and C) .
-- _xor_
eq false xor A = A .
eq     A xor A = false .
-- _or_
eq false or A = A .
eq  true or A = true .
eq     A or A = A .
eq     A or B = (A and B) xor A xor B .
-- not_
eq not A = A xor true .
-- _implies_
eq A implies B = (A and B) xor A xor true .
-- _iff_
eq A iff B = A xor B xor true .
-- ---------------------------------------------

A Boolean expression (an expression/term of sort Bool) is defined to
be in xor-and normal form iff (if and only if) it is expressed as:

        c_1 xor c_2 xor ... xor c_m  (if m=0 then false)

without any dupulication of c_i (i.e. c_j = c_k does not hold for any
different j and k; notice that c_j = c_k is determined considering
associative and commutative atributes of predicate (_ and _), that is
modulo associativity and commutativity), and each c_p (p=1...m) is
expressed as:

       b_l and b_2 and ... and b_n(p) (if n(p)=0 then true)

for some Boolean variables b_i (i = 1...n(p)) without any duplication
(i.e. b_j=b_k does not hold for any different j and k).

(2-1) Prove that any Boolean expression which is composed of Boolean
      variables and the Boolean operations of (_ and _), (_ xor _), (_
      or _), (not _), (_ implies _), (_ iff _) can be reduced to a
      Boolean expression in xor-and normal form.  Hint: See Lecture
      Note 3 (Reasoning by Rewriting).

The value tables for the predicates (_ and _), (_ xor _), (_ or _),
(not _), (_ implies _), (_ iff _) are defined as follows by the
equations of BOOL.

-- ---------------------------------------------
-- Logical Value Talbes for BOOL Predicates ----
-- ---------------------------------------------
-- -----------------------
(true and true)   = true
(true and false)  = false
(false and false) = false
-- -----------------------
(true xor true)   = false
(true xor false)  = true
(false xor false) = false
-- -----------------------
(true or true)   = true
(true or false)  = true
(false or false) = false
-- -----------------------
(not true)  = false
(not false) = true
-- --------------------------
(true implies true)   = true
(true implies false)  = false
(false implies true)  = true
(false implies false) = true
-- --------------------------
(true iff true)   = true
(true iff false)  = false
(false iff true)  = false
(false iff false) = true
-- --------------------------

By using these tables, any Boolean expression which is composed of n
Boolean variables b_l, b_2 ... b_n and the Boolean operations of (_
and _), (_ xor _), (_ or _), (not _), (_ implies _), (_ iff _) is
considered to define an n arguments Boolean function. That is, if you
assign "true" or "false" to each of variables b_l, b_2, ..., and b_n
in the expression the expression evaluates to "true" or "false".

Two Boolean expressions bexp_1 and bexp_2 which are composed of n
Boolean variables b_l, b_2, ... b_n and the above 6 Boolean operations
are defined to be equal, written as (bexp_1 =eq= bexp_2), iff they
define the same n arguments Boolean function.

(2-2) Prove that the following assertion hold for any two Boolean
      expression bexp_1 and bexp_2 in xor-and normal form with n
      Boolean variables b_l, b_2 ... b_n.

	      (bexp_1 = bexp_2) iff (bexp_1 =eq= bexp_2)

      Notice that (bexp_1 = bexp_2) is determined modulo associativity
      and commutativity of (_ and _) and (_ xor _).

Notice that (2-1) and (2-2) constitute a decision procedure for
determining equivalence (i.e. equal as Boolean functions) of Boolean
expressions.

=======================================================================
			     Problem 3
=======================================================================
Integers are modeled as the following CafeOBJ specification BASIC-INT.

mod! BASIC-INT {
  [Zero PsInt NgInt < Int]  
  op 0 : -> Zero {constr}	
-- successor +1
  op s_ : Zero -> PsInt {constr}   
  op s_ : PsInt -> PsInt {constr}  
  op s_ : Int -> Int {constr}
-- predecessor -1
  op p_ : Zero -> NgInt {constr} 
  op p_ : NgInt -> NgInt {constr} 
  op p_ : Int -> Int {constr}
--  
  eq s p I:Int = I .
  eq p s I:Int = I . 
}

By induction with respect to the number of occurrences of (..s p..) or
(..p s..) in a term in the sort Int, it is proved that any element in
Int is reduced to an element of Zero (= {0}), PsInt (= {s 0,s s 0,s s
s 0,...}), or NgInt (= {p 0,p p 0,p p p 0,...}).

Plus operation over the Int is defined as the following specification
INT+.

mod! INT+ {
  protecting (BASIC-INT)
  op (_ + _) : Int Int -> Int
  vars I J : Int 
  eq     0 + J = J .
  eq (s I) + J = s(I + J) . 
  eq (p I) + J = p(I + J) . 
}

(3-1) Prove that the specification INT+ is terminating, confluent, and
      sufficiently complete.  Hint: See the Lecture Note 3 (Reasoning
      by Rewriting).

(3-2) Write proof scores which verify the following associativity and
      commutativity of the plus operation (_ + _).

        **> Associativity of Plus
        **> AP: eq (I:Int + J:Int) + K:Int = I + (J + K) .
      and
        **> Commutativity of Plus
        **> CT: eq I:Int + J:Int = J + I .

By assuming that associativity and commutativity of (_ + _) is proved,
the following specification INT+ac can be used instead of INT+ .

mod! INT+ac {
  protecting (BASIC-INT)
  op (_ + _) : Int Int -> Int {assoc comm}
  vars I J : Int 
  eq     0 + J = J .
  eq (s I) + J = s(I + J) . 
  eq (p I) + J = p(I + J) . 
}

Times operation (_ * _) over the sort Int is defined by the following
specifications INT- and Int* .

mod! INT- {
  pr(INT+ac)
  op (- _) : Int -> Int
  eq - 0 = 0 .
  eq - (s I:Int) = p (- I) .
  eq - (p I:Int) = s (- I) .
  op (_ - _) : Int Int -> Int 
  eq I:Int - J:Int = I + (- J) .
}

mod! INT* {
  pr(INT-)
  op (_ * _) : Int Int -> Int
  vars I J : Int 
  eq     0 * J = 0 .
  eq (s I) * J = (I * J) + J .
  eq (p I) * J = (I * J) - J . 
}

(3-3) Prove that the specification INT- and INT* is terminating,
      confluent, and sufficiently complete.  Hint: See the Lecture
      Note 3 (Reasoning by Rewriting).

(3-4) Write proof scores which verify the following three properties.

        **> Left Distributive Law
        **> LDL: eq (I:Int + J:Int) * K:Int = (I * K) + (J * K) .
      and
        **> Associativity of Times
        **> AT: eq (I:Int * J:Int) * K:Int = I * (J * K) .
      and
        **> Commutativity of Times
        **> CT: eq I:Int * J:Int = J * I .

=======================================================================
			      Problem 4
=======================================================================

(4-1) Write proof scores of all lemmas (lemmas in abp.mod file of
      Lecture Note 7) on data types used in the ABP case study.  If
      you think that the original specifications should be changed,
      point out the needed changes.

(4-2) Write proof scores of inv2, inv8 and inv10 of ABP.

=======================================================================
			      Problem 5
=======================================================================

Conjecture a non-trivial invariant on ABP that have never been seen in
the ABP case study, and write a proof score of the invariant and proof
scores of lemmas if any.

=======================================================================
			     end end end
=======================================================================