Formal Methods -- SE304/CS407 -- Lab 5

Part 1 - Ambiguous Terms

• Modules
  • SIMPLE-NAT.mod
  • SIMPLE-INT.mod
• Commands
  • input SIMPLE-NAT
  • input SIMPLE-INT
  • parse in SIMPLE-INT : M + M + M .
• Question
  • Explain why you are offered two choices.

Part 2 - Develop a module

• Develop a module which specifies a recursive definition of Natural numbers. Include:
  • successor - s
  • addition - +
  • multiplication - *
• Your module must be able to correctly reduce the following two terms:
  • (s s 0) + (s s s s 0)
  • (s s s 0) * (s s s s s 0)

Links

• CafeOBJ manual

Home