Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Specification Language

⚠️ Work in Progress: This section is under development.

This chapter covers advanced specification techniques in Ursus.

Topics to be Covered

Specification Levels

  • Function specifications
  • Contract specifications
  • System specifications
  • Protocol specifications

Temporal Logic

  • LTL (Linear Temporal Logic)
  • CTL (Computation Tree Logic)
  • Temporal properties
  • Liveness properties

Refinement

  • Refinement relations
  • Simulation proofs
  • Bisimulation
  • Abstraction

Composition

  • Compositional specifications
  • Modular verification
  • Assume-guarantee reasoning
  • Contract composition

Specification Patterns

Safety Properties

  • Invariants
  • Type safety
  • Memory safety
  • Access control

Liveness Properties

  • Termination
  • Progress
  • Fairness
  • Responsiveness

Coming Soon

This section will include:

  • Specification examples
  • Verification techniques
  • Proof patterns
  • Tool support

See Also