| precondition | statement | postcondition |
|---|---|---|
|
statement
|
|
condition
|
condition
|
| guards |
|---|
| precondition |
|---|
| condition |
| statements |
|---|
| postcondition |
|---|
| condition |
| precondition | postcondition |
|---|---|
|
condition
|
condition
|
| statement 1 | intermediate condition | statement 2 |
|---|---|---|
| invariant | guard | variant |
|---|---|---|
| precondition | loop statement | postcondition |
|
condition
|
condition
|
| weak precondition | Statement | strong postcondition |
|---|---|---|
About
CorC is an editor to construct algorithms following the Correctness-by-Construction approach.
Correctness-by-Construction (CbC) is an approach to incrementally create correct programs. Guided by pre-/postcondition specifications, a program is created using refinement rules, guaranteeing the resulting implementation is correct. We implemented a graphical and textual IDE to create programs following the CbC approach. Starting with an abstract specification, our tool supports CbC developers to refine a program by a sequence of refinement steps and to verify the correctness of these refinement steps using a theorem prover.