CN Tutorials¶
These tutorials introduce CN through a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures.
Warning
These tutorials focus on verifying CN specifications and do not cover runtime testing. Runtime testing will be introduced in future documentation.
Source files¶
The source files for all the exercises and examples below can be downloaded from here.
Tutorials¶
- Basic usage
- Pointers and simple ownership
- Ownership of compound objects
- Arrays and loops
- Defining predicates
- Allocating and deallocating memory
- Lists
- Working with external lemmas