blob: 4ffb49d3f541f3ca3ffdafdac38b514a932e58a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
+++
title = "Specification for proofs"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5e"]
forwardlinks = []
zettelid = "3a5f"
+++
To build a proof of an algorithm, it can be useful to have a
specification of the algorithm first, and then prove that this
specification has the property that one wants to prove. This can be
useful because the specification is often at a higher level than the
algorithm itself, and it can therefore be easier to identify it's
behaviour in the proofs.
However, one more step is needed if this approach is taken, because it
also has to be proven that the algorithm that one designed does indeed
implement the specification that was designed. However, this only has to
be done once, and thereafter the specification can be used to prove any
other useful properties.
A concrete example for this is the proof from Cminor to RTL in CompCert.
At the lowest level, there is an implementation of an algorithm that
does this translation. However, then there is a specification of this
algorithm using `Inductive` types. The latter is then used to prove that
the semantics before the translation are equivalent to the semantics
after the translation.
|
