Recitation R14
- Program Correctness
Fall 2013
CS160: Foundations in Programming
The purpose of this lab is to:
- Discuss program verification in terms of practical testing techniques.
- Discuss program correctness in terms of the theory presented in this class.
- Work on RamCT Quiz 5 - Program Correctness
Pragmatic Testing
You won't see this material until upper level software engineering classes, but it should be incorporated
into a slide set for this class. Some of this is fact and some is based on the observations of the instructor.
However, many of these statements are commonly accepted in the areas of industry where I have worked:
- It is often said that software developers are notoriously poor at testing their own code.
- Why? Because developers aren't objective - they think they know exactly how it should work.
- Furthermore they have certain expectations of users that fail to account for the unexpected.
- And that's assuming the developers even have time to look for defects!
- Quality assurance and testing activities are often curtailed in the real world because of schedule.
- Quality engineers had traditionally not had the highest status or pay.
- Despite this, quality software depends on meticulous testing, and successful software companies do it well.
- Amount of time spent verifying programs should probably exceed development time.
- Testing should be incorporated from the very beginning to the very end of the development cycle.
A recent trend in software engineering is Test-Driven Development (TDD), which specifies that
tests be written before code. The philosophy behind this is that you can only truly understand (and define)
the functionality of a piece of code by defining how it is tested.
Many different approaches to testing exist, as shown below:
- Unit Testing: Test every method or subroutine in the software individually.
- Module Testing: Test the behavior of each module, taking into account state (member variables).
- Integration Testing: Test the interaction between modules, i.e. how does one class use another.
- System Testing: Test the software as a typical user would test it.
- Stress Testing: Try to overload the software, pushing it beyond normal usage.
- Code Coverage: Make sure that every line of software is tested.
- Branch Coverage: Test all branches through the software, i.e. every if/else-if/if in a conditional, every case in a switch, etc.
- Definition-Use: Test every path from the assignment of a variable to its use.
- Sanity Testing: Make sure the program doesn't crash immediately.
- Centerline Testing: Test using values that are expected.
- Boundary Testing: Test values that may cause problems: -1, 0, 1, zero length strings or arrays, null pointers.
- Error Testing: Test all the failure conditions to verify error paths in code.
- Regression Testing: Making sure that software does not go backwards by testing against an oracle.
- Platform Testing: Making sure that software is truly cross-platform (Windows, Mac, Linux).
And there are many, many, many more ways to test software: for example installation/acceptance/alpha/beta testing.
The link to Wikipedia page on software testing is
here.
This is an area that occupies lots of software engineering researchers and developers in industry.
Program Correctness
The key ideas from the theoretical viewpoint of program correctness are as follows:
- Pre-Conditions characterize the input expected by a method, i.e. show the limitations of the code.
- Post-Conditions characterize the output expected from a method, i.e. show the functionality of the code.
- We can use these to prove program correctness, or more practically, to verify method behavior.
- We can account for pre and post-conditions even for different paths through the code (Conditional Rule).
- We can account for pre and post-conditions for iterative control such as loops (Loop Invariants).
- We can chain pre and post-conditions for individual methods to prove correctness for entire programs (Composition Rule).
Work on RamCT Quiz 5 with help from the TA
Checkin with the TA and show your score on RamCT Quiz 5 to get credit for this lab.
© 2013 CS160 Colorado State University. All Rights Reserved.