Formal Methods -- SE304/CS407 -- Lab 7

Continuous Assessment Results

Come over to me at any point during today's lab for your results-to-date. Today's lab and next week's lab will also be included in your continuous assessment marks.

Proofs

• For the following module:
  

  module SIMPLE-NAT {

  [Zero NzNat < Nat]
  
  op 0 : -> Zero
  op s : Nat -> Nat
  op _+_ : Nat Nat -> Nat
  
  vars X, Y : Nat
  eq 0 + X = X .
  eq s(X) + Y = s(X + Y) .
  

  }

  open SIMPLE-NAT .
  op a : -> Nat .
  --> Should reduce to 0
  red 0 + 0 .
  
  --> Inductive hypothesis
  eq a + 0 = a .
  
  --> Conclusion - should reduce to s(a)
  red s(a) + 0 .
  close

1. Why is a declared as a constant (operator) rather than as a variable?
2. Add a proof of the associativity of '+'.

Operator Attributes

• Add the operators
  • - (pseudo-minus discussed in lectures)
  • *
  • %
• What is the Identity of the * operator? Use an operator attribute to include this in your specification.
• Identify one operator which could be defined as associative. Use an operator attribute to include this in your specification.
• Identify one operator which could be defined as commutative. Use an operator attribute to include this in your specification.

Stack Module

• Create a module which describes a stack of SIMPLE-INTs

---

To hand up:

Please note: This lab and next week's lab are worth more marks than previous labs.

• Paragraph answering proof question 1
• CafeOBJ code answer to proof question 2
• CafeOBJ code answer to operator attributes question
• Stack module (CafeOBJ code)

These must be handed up by the end of today's lab.

---

Home