Assignment of i613 Formal Methods

You are given four problems. Solve all of them.

- Put all of your specifications and proof scores in one file and
check if CafeOBJ successfully accepts the file with command "in". The
file name should be your (family) name followed by your student ID and
the standard extension ".mod". For example, if your (family) name is
Ishikawa and your student ID is 012345, then the file name should be
"ishikawa01234.mod".

- Write a report on your solutions of the problems in plain text.

- Submit your report and file to the lecturers by email by the
designated deadline. The report (in plain text) should be written in
the main body of the email, and the file should be attached in the
email. The subject of the email should be "i613-0912-Report".


Problem 1 (score 5). Given the following module (LIST) in which
generic lists are specified:

mod! LIST(M :: TRIV-EQ-LT) {
  pr(NAT)
  [Nil NnList < List]
  op nil : -> Nil {constr}
  op _|_ : Elt.M List -> NnList {constr}
  op _=_ : List List -> Bool {comm}
  op top : NnList -> Elt.M
  op last : NnList -> Elt.M
  op _@_ : List List -> List
  op _@_ : NnList List -> NnList
  op _@_ : List NnList -> NnList
  op _@_ : NnList NnList -> NnList
  op sorted? : List -> Bool
  vars E E' : Elt.M
  var N : Nat
  vars L L1 L' L'' : List
  vars NL NL' : NnList
  -- _=_
  eq (L = L) = true .
  eq (nil = (E | L)) = false .
  eq ((E' | L') = (E | L)) = (E' = E) and (L' = L) .
  -- top
  eq top(E | L) = E .
  -- last
  eq last(E | nil) = E .
  eq last(E | E' | L) = last(E' | L) .
  -- _@_
  eq nil @ L1 = L1 .
  eq (E | L) @ L1 = E | (L @ L1) .
  -- sorted?
  eq sorted?(nil) = true .
  eq sorted?(E | nil) = true .
  eq sorted?(E | E' | L)
     = (not E' < E) and sorted?(E' | L) .
  -- Some Simple Lemmas on Lists
  eq last(E | NL) = last(NL) .
  eq last(L @ NL) = last(NL) .
  eq top(NL @ NL') = top(NL) .
  op eq-of-tops : Elt.M List List List -> Bool
  eq eq-of-tops(E,L,L',L'')
     = (top(L @ (E | L')) = top(L @ (E | L''))) .
}

where module TRIV-EQ-LT is as follows:

mod* TRIV-EQ-LT {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
  op _<_ : Elt Elt -> Bool
  op irref-lt : Elt Elt -> Bool
  op tran-nlt : Elt Elt Elt -> Bool
  vars E E' E'' : Elt
  eq (E = E) = true .
  eq irref-lt(E,E') = E < E' implies  (not E' < E) .
  eq tran-nlt(E,E',E'')
     = (not E < E') and (not E' < E'') implies (not E < E'') .
}

Prove the following with CafeOBJ:

\forall NL1,NL2:NnList,
sorted?(NL1 @ NL2)
iff
(sorted?(NL1) and sorted?(NL2) and (not top(NL2) < last(NL1)))

Note that you can use the following induction scheme:

(\forall E:Elt, p(E | nil)),
(\forall E,E':Elt, L:List, p(E' | L) implies p(E | E' | L))
---------------------------------------------------------------
(\forall NL:NnList, p(NL))

Note also that you can use the following lemmas on lists in Problems
1,2,3 without proving them:

- \forall E:Elt, NL:NnList, last(E | NL) = last(NL)
- \forall L:List, NL:NnList, last(L @ NL) = last(NL)
- \forall NL,NL':NnList, top(NL @ NL') = top(NL)
- \forall E:Elt, L,L',L'', top(L @ (E | L')) = top(L @ (E | L''))

and the following axioms on _<_ in Problems 1,2,3:

- \forall E,E':Elt, E < E' implies  (not E' < E)
- \forall E,E',E'':Elt, (not E < E') and (not E' < E'') implies (not E < E'')

These lemmas and axioms are already written in LIST and TRIV-EQ-LT,
respectively.


Problem 2 (score 10). Given the following module (BSTREE) in which
generic binary search trees are specified:

mod! BSTREE(K :: TRIV-EQ-LT) {
  pr(LIST(K)) 
  [BSLeaf BSNlTree < BSTree]
  op leaf : -> BSLeaf {constr}
  op node : BSTree BSTree Elt.K -> BSNlTree {constr}
  op insert : Elt.K BSTree -> BSNlTree
  op bst2list : BSTree -> List
  op bst2list : BSLeaf -> Nil
  op bst2list : BSNlTree -> NnList
  vars K K1 : Elt.K
  var N : Nat
  vars LT RT : BSTree
  -- insert
  eq insert(K,leaf) = node(leaf,leaf,K) .
  eq insert(K,node(LT,RT,K1))
     = if K = K1 then node(LT,RT,K1)
       else (if K <.K K1 then node(insert(K,LT),RT,K1)
             else node(LT,insert(K,RT),K1) fi) fi .
  -- bst2list
  eq bst2list(leaf) = nil .
  eq bst2list(node(LT,RT,K))
     = bst2list(LT) @ (K | bst2list(RT)) .
}

Prove the following with CafeOBJ:

\forall E,E',E2:Elt, T:BSTree,
(not E' < E) and (not E' < last(E2 | bst2list(T)))
implies
(not E' < last(E2 | bst2list(insert(E,T))))

\forall E,E',E2:Elt, T:BSTree, L:List,
(not E < E') and (not top(bst2list(T) @ (E2 | L)) < E')
implies
(not top(bst2list(insert(E,T)) @ (E2 | L)) < E')


Problem 3 (score 20). Given the following module (BST-SORT) in which a
sorting algorithm using binary search trees is implemented:

mod! BST-SORT(M :: TRIV-EQ-LT) {
  pr(BSTREE(M))
  op bstsort : List -> List
  op sbsts : List BSTree -> BSTree
  var E : Elt.M
  var L : List
  var T : BSTree
  eq bstsort(L) = bst2list(sbsts(L,leaf)) .
  eq sbsts(nil,T) = T .
  eq sbsts(E | L,T) = sbsts(L,insert(E,T)) .
}

Prove the following with CafeOBJ:

\forall L:List, sorted?(bstsort(L))

Note that you need to conjecture some other lemmas.


Problem 4 (score 30). Prove with CafeOBJ that a mutual exclusion
protocol (called Ticket) enjoys the mutual exclusion property. The
pseudo-program executed by each process i in Ticket is as follows:

Loop {
    Remainder Section
  rs: ticket[i] := atomicInc(vm);
  ws: repeat until ticket[i] = turn;
    Critical Section
  cs: turn := turn + 1;
}

where atomicInc(x) atomically (indivisibly) increments the value
contained in a variable x and returns the old value of x, vm and turn
whose types are natural numbers are shared by all processes, and
ticket[i] whose type is natural numbers is local to process
i. Initially, each process is at label rs, vm is 0, turn is 0, and
each ticket[i] is an arbitrary number.