Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_24 [2007/07/01 18:29] kremena.diatchka |
sav07_lecture_24 [2007/07/01 18:37] kremena.diatchka |
||
---|---|---|---|
Line 499: | Line 499: | ||
- [[http://www.brics.dk/PALE/|Pointer Assertion Logic Enginer]] - verification condition generation, MSOL over strings - no loop invariant inference | - [[http://www.brics.dk/PALE/|Pointer Assertion Logic Enginer]] - verification condition generation, MSOL over strings - no loop invariant inference | ||
- [[http://www.informatik.uni-freiburg.de/~wies/papers/verifying-complex-properties.pdf|Verifying Complex Properties using Symbolic Shape Analysis]] - loop invariant inference, wider class of structures | - [[http://www.informatik.uni-freiburg.de/~wies/papers/verifying-complex-properties.pdf|Verifying Complex Properties using Symbolic Shape Analysis]] - loop invariant inference, wider class of structures | ||
+ | |||
Line 529: | Line 530: | ||
== List example == | == List example == | ||
- | To prove properties about a list, sequences are used as abstract values. In the following example, $\alpha$ and $\beta$ denote sequences, and $\epsilon$ denotes an empty sequence. To describe the representation of a singly-linked list we write $\mbox{list}(\alpha,i,j)$ where where there is a list segment from //i// to //j// representing the sequence $\alpha$ | + | To prove properties about a list, sequences are used as abstract values. In the following example, $\alpha$ and $\beta$ denote sequences, and $\epsilon$ denotes an empty sequence. To describe the representation of a singly-linked list we write $\mbox{list}(\alpha,i,j)$ where where there is a list segment from //i// to //j// representing the sequence $\alpha$. |
+ | |||
+ | {{list_segments.png|}} | ||
Inductive definitions: | Inductive definitions: |