Lecture overview -- Keyboard shortcut: 'u'  Previous page: Correctness -- Keyboard shortcut: 'p'  Next page: Specification with preconditions and postconditions [Section] -- Keyboard shortcut: 'n'  Lecture notes - all slides and notes together  slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Help page about these notes  Alphabetic index  Course home  Page 4 : 32
Object-oriented Programming in C#
Contracts and Assertions
Specifications

A program specification is a definition of what a computer program is expected to do [Wikipedia].

What - not how.

 

  • Formal techniques for specification of abstract datatypes

    • Algebraic specifications

      • Equations that define how certain operations work on constructor expressions

    • Axiomatic specifications

      • Logical expressions - assertions - associated with classes and operations

      • Often divided into invariants, preconditions, and postconditions

/user/normark/oop-csharp-1/sources/other-sources/adt/stack.gasAn algebraic specification of a stack.


/user/normark/oop-csharp-1/sources/notes/includes/sqrt-specificationAn axiomatic specification of the squareroot function.