diff options
Diffstat (limited to 'content/zettel/3a5d.md')
| -rw-r--r-- | content/zettel/3a5d.md | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/content/zettel/3a5d.md b/content/zettel/3a5d.md new file mode 100644 index 0000000..c5b8d3f --- /dev/null +++ b/content/zettel/3a5d.md @@ -0,0 +1,18 @@ ++++ +title = "Proving correctness of the specification" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a5c"] +forwardlinks = ["3a5e"] +zettelid = "3a5d" ++++ + +Have a backwards simulation implies that the output *C* will follow the +same specification as the source program. This can be seen by the fact +that the backwards simulation is just a stronger statement about +correctness compared to following a simulation. For example, if a +specification says that a program should output a number greater than +10, the source could output 11 and the compiled program could output 12. +These both follow the specification, but would not hold under backward +simulation, where the two values would have to be the same. |