Loading...
Please wait, while we are loading the content...
Similar Documents
15-414 : Bug Catching : Automated Program Verification Lecture Notes on Programs with Arrays
| Content Provider | Semantic Scholar |
|---|---|
| Author | Fredrikson, Matt Platzer, André |
| Copyright Year | 2017 |
| Abstract | The previous lecture focused on loops, starting with axioms and leading to a derived rule that allows us to simplify reasoning about loops to reasoning about the behavior of a single iteration of their bodies. We worked an example involving a program that uses loops to compute the square of a number, and found that much of the difficulty in reasoning about loops lies in finding a suitable invariant. Loops are frequently used to compute over a sort of programming element that we haven’t introduced yet, namely arrays. Arrays are an important data structure in imperative programming, enabling us to implement things that we couldn’t otherwise. However, they introduce significant complexity into programs’ behavior, so sound reasoning about their use is crucial. Today we will introduce arrays into our language, and use our semantics to argue the correctness of the binary search code we discussed in the first lecture. Along the way, we will build more experience in finding suitable loop invariants for increasingly complex code, and in all likelihood, learn to appreciate the benefits of using an SMT solver to complete our proofs. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~15414/lectures/06-arrays.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
