Summary
Summary System Development Methods (INFOBSOM)
- Course
- Institution
All information for the final exam
[Show more]
Seller
Follow
IsabelleU
Reviews received
Content preview
SOM SV Final501 – 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
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card or Stuvia-credit for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller IsabelleU. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for $8.10. You're not tied to anything after your purchase.
Can Stuvia be trusted?
4.6 stars on Google & Trustpilot (+1000 reviews)
67096 documents were sold in the last 30 days
Founded in 2010, the go-to place to buy study notes for 14 years now