Summary System Development Methods (INFOBSOM)

SOM SV Final

501 – Design by contract, Hoare logic
➢ How to design correct software?
➢ Main issue of software correctness is that it meets its specifications
➢ Software crisis: machines have become more powerful and gigantic → programming equally
gigantic problem.
Hoare logic
➢ {P} C {Q}
o Provided the precondition P holds at the state before the execution of program C, then
the postcondition Q will hold afterwards, or C does not terminate.
➢ Designing a logic → rules to reason about programs according to Hoare:
o Skip: the simplest rule is for the skip command, that does nothing
▪ {P} skip {P}
• {x > 3} skip {x>3} is valid
o Assignment
{P[e/x]} x := e {P}
▪ The precondition for
x := e {P}
▪ Is uniquely determined by
{P[e/x]}
▪ i.e. the predicate P where each x is substituted by e
• bv {x+1 <= N} x := x + 1 {x <= N} is valid
o Composition
▪ suppose we know that
• {P} c1 {Q} and {Q} c2 {R}
▪ What can we deduce about c1;c2?
• {P} c1; c2 {R}
▪ Bv if we have {x+1=43) y := x+1 {y=43}
And {y=43} z := y {z=43}
▪ We can deduce {x+1=43} y := x+1; z:= y {z=43}
o Conditional rule
▪ Suppose we know
▪ Then the following also holds: {P} if B then S else
T endif {Q}
▪ {0<=x<=15} if x<15 then x:=x+1 else x:= 0 endif
{0<=x<=15}
▪ Then part:
{0<=x<=15 and x<15} x:=x+1 {0<=x<=15}, or
simplified
{0<=x<=15} x:=x+1 {0<=x<=15}
▪ Then part has a stronger precondition than the
whole if statement!
o Consequence rule
▪ If we know
▪ P1 → P2, { P2}S{Q2}, Q2 → Q1
▪ Then: {P1}S{Q1}


1

, ▪ Preconditions may be strengthened,
postconditions may be weakened
➢ You can add more rules, some of which can be tricky. Using
these rules you suddenly have the ability to prove statements
about your program → major breakthrough
Contracts
➢ In most cases, finding the bug requires much more effort than
repairing the bug
➢ IRL, we make contracts all the time. Contracts establish some agreement between two parties:
o Each party expects certain benefits, but is willing to incur obligations to obtain them
o These benefits and obligations are documented in a contract document
➢ This contract document protects both parties
Assertions in code
➢ Python provides methods to help write pre- and postconditions in your code.
def reciprocal (x: int) -> float:
return 1/x
➢ This code can fail (call it with 0)
def reciprocal (x: int) -> float:
assert x != 0
return 1/x
➢ If another method calls reciprocal(0), the code will throw an exception and show the call
stack. Variants exist that will allow you to display custom error messages, etc.
➢ Besides checking preconditions, we ca also use assertations to check that our code produces
the correct result:
def sort(xs: List[int]) -> List[int]:
result = …
assert is_sorted(result)
return result
➢ Now if anybody changes the method body, introducing a bug, our program will fail when run
Contracts in software design
➢ The same ideas can be applied to software design
➢ Decorate methods with assertations, stating which contractual obligations:
o It requires of the caller
o It ensures for the caller
➢ These assertations form an important piece of documentation, specifying what a method
should do
➢ Why write pre- and postconditions in use cases?
o Can help developers figure out what is really going on, and under which conditions
they can abort
o First step towards (automated) testing
o Provides information for writing contracts
o Forces you (software designer) to think about what is really going on
➢ Defensive programming as a result of taking these ideas seriously and assume that everyone
is out to crash your code
o Never trust input → if you assume the argument is greater than 0, add an assertation
to check this
o Fail early and openly → check any preconditions before entering the method body


2