blob: c5b8d3f4aca9698cdc8c4c157047c67d864ea13f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
