Init
This commit is contained in:
17
README.md
Normal file
17
README.md
Normal file
@ -0,0 +1,17 @@
|
||||
# Hoare Test
|
||||
|
||||
This project is me teaching myself formal verification using Hoare logic in Rust
|
||||
|
||||
## What is Hoare logic
|
||||
|
||||
Hoare logic is about proving programs work correctly using this format:
|
||||
```
|
||||
{P} code {Q}
|
||||
```
|
||||
|
||||
Where:
|
||||
- P = what must be true before the code runs (precondition)
|
||||
- code = the actual code I'm testing
|
||||
- Q = what will be true after the code runs (postcondition)
|
||||
|
||||
It's essentially making promises about what the code does, then having the compiler check that I keep those promises.
|
Reference in New Issue
Block a user