Samenvatting
Samenvatting Systeemontwikkelingsmethoden (INFOBSOM)
- Instelling
- Universiteit Utrecht (UU)
Alle stof voor de final
[Meer zien]Voorbeeld 2 van de 13 pagina's
Voorbeeld 2 van de 13 pagina's
In winkelwagengesponsord bericht van onze partner
Voorbeeld van de inhoud
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
Voordelen van het kopen van samenvattingen bij Stuvia op een rij:
Verzekerd van kwaliteit door reviews
Stuvia-klanten hebben meer dan 700.000 samenvattingen beoordeeld. Zo weet je zeker dat je de beste documenten koopt!
Snel en makkelijk kopen
Je betaalt supersnel en eenmalig met iDeal, creditcard of Stuvia-tegoed voor de samenvatting. Zonder lidmaatschap.
Focus op de essentie
Samenvattingen worden geschreven voor en door anderen. Daarom zijn de samenvattingen altijd betrouwbaar en actueel. Zo kom je snel tot de kern!
Veelgestelde vragen
Wat krijg ik als ik dit document koop?
Je krijgt een PDF, die direct beschikbaar is na je aankoop. Het gekochte document is altijd, overal en oneindig toegankelijk via je profiel.
Tevredenheidsgarantie: hoe werkt dat?
Onze tevredenheidsgarantie zorgt ervoor dat je altijd een studiedocument vindt dat goed bij je past. Je vult een formulier in en onze klantenservice regelt de rest.
Van wie koop ik deze samenvatting?
Stuvia is een marktplaats, je koop dit document dus niet van ons, maar van verkoper IsabelleU. Stuvia faciliteert de betaling aan de verkoper.
Zit ik meteen vast aan een abonnement?
Nee, je koopt alleen deze samenvatting voor €7,49. Je zit daarna nergens aan vast.
Is Stuvia te vertrouwen?
4,6 sterren op Google & Trustpilot (+1000 reviews)
Afgelopen 30 dagen zijn er 67096 samenvattingen verkocht
Opgericht in 2010, al 14 jaar dé plek om samenvattingen te kopen