Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
1
Software System Design and Implementation
Property Based Testing Practice
Curtis Millar
CSE, UNSW (and Data61) 17 June 2020
Exercise 1
Property Based Testing Proofs and Tests Homework Consultations
2
1
2 3
Simple Picture: add the chimney and smoke
Moving Objects: implement movePictureObject
Generating a Picture: generate pictures of circles using simpleCirclePic
Exercise 1
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Property Based Testing
Key idea: Generate random input values, and test properties by running them.
Example (QuickCheck Property)
prop_reverseApp xs ys =
reverse (xs ++ ys) == reverse ys ++ reverse xs
Haskell’s QuickCheck is the first library ever invented for property-based testing. The concept has since been ported to Erlang, Scheme, Common Lisp, Perl, Python, Ruby, Java, Scala, F#, OCaml, Standard ML, C and C++.
3
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Mersenne Prime Example
Example (Demo Task)
4
The nth Mersenne number Mn = 2n−1.
M2, M3, M5 and M7 are all prime numbers. Conjecture: ∀n.prime(n) =⇒ prime(2n−1)
Let’s try using QuickCheck to answer this question.
After a small number of guesses and fractions of a second, QuickCheck found a counter-example to this conjecture: 11.
It took humanity about two thousand years to do the same.
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Semigroup and Monoid Properties
Last week we proved by hand that a list forms a semigroup with ++ as its associative operator and a monoid with [] as its identity element.
We can show the same properties much faster (although less completely) with property based testing.
QuickCheck Properties
— Semigroup laws
prop_listAssociative xs yz zs = ((xs ++ ys) ++ zs) == (xs ++ (ys ++ zs))
— Monoid laws
prop_listLeftIdentity xs = xs == [] ++ xs
prop_listRightIdentity xs = xs == xs ++ []
5
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Reverse Involution
Last week we also proved by hand that the reverse function is an involution. This took over twenty minutes.
Let’s see how long it takes QuickCheck.
QuickCheck Property
prop_reverseInvolution xs = reverse (reverse xs) == xs
6
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Ransom Note Example
Example (Demo Task)
7
Given a magazine (in String form), is it possible to create a ransom message (in String form) from characters in the magazine.
canMakeRansom :: RansomNote -> Magazine -> Bool
1 Write a specification
2 Create an efficient implementation
3 Test the implementation
In Haskell.
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
Graphics
Write some specifications for the following functions, use them to create properties, and then test an implementation.
1 Horizontal flip
2 Vertical flip
3 Rotate 180 degrees
Example (Demo Task)
Implement the above for a single Path. (You might want to try and implement these for other PictureObject constructors or for an entire Image as self-practice.) In Haskell.
8
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
9
Proofs:
Proofs
Proofs must make some assumptions about the environment and the semantics of the software.
Proof complexity grows with implementation complexity, sometimes drastically.
If software is incorrect, a proof attempt might simply become stuck: we do not always get constructive negative feedback.
Proofs can be labour and time intensive ($$$), or require highly specialised knowledge ($$$).
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
10
Compared to proofs:
Testing
Tests typically run the actual program, so requires fewer assumptions about the language semantics or operating environment.
Test complexity does not grow with implementation complexity, so long as the specification is unchanged.
Incorrect software when tested leads to immediate, debuggable counterexamples. Testing is typically cheaper and faster than proving.
Tests care about efficiency and computability, unlike proofs.
We lose some assurance, but gain some convenience ($$$).
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
11
Verification versus Validation
”Testing shows the presence, but not the absence of bugs.”
– Dijkstra (1969)
Testing is essential but is insufficient for safety-critical applications.
Exercise 1
Property Based Testing Proofs and Tests Homework Consultations
12
1
2 3
Last week’s quiz is due on Friday. Make sure you submit your answers.
The second programming exercise is due by the start if my next lecture (in 7 days). This week’s quiz is also up, it’s due next Friday (in 9 days).
Homework
Exercise 1 Property Based Testing Proofs and Tests Homework Consultations
13
Consultations
Tomorrow, 9am to 11am on Blackboard Collaborate
Link on course website.
Be ready to share your screen with REPL (ghci or stack repl) and editor set up.