diff options
author | n.ramanathan14 <n.ramanathan14@imperial.ac.uk> | 2020-11-18 17:10:24 +0000 |
---|---|---|
committer | overleaf <overleaf@localhost> | 2020-11-18 17:15:23 +0000 |
commit | 416227d361e75d05e87e6dde469c6cce76db874d (patch) | |
tree | e488dd237e8c4e2981db17b04cd2517db9b4ef7e /proof.tex | |
parent | d1f9f640ed03e9ad2a28b90578de416eed2ad707 (diff) | |
download | oopsla21_fvhls-416227d361e75d05e87e6dde469c6cce76db874d.tar.gz oopsla21_fvhls-416227d361e75d05e87e6dde469c6cce76db874d.zip |
Update on Overleaf.
Diffstat (limited to 'proof.tex')
-rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -14,7 +14,7 @@ To prove this top-level theorem, a forward simulation has to be done between eac \subsection{Specification} -To simplify the proof, instead of using the translation algorithm as an assumption, as was done in the backward simulation stated above, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness. For example, for the translation from 3AC to HTL, the translation might be defined using the following function: $\yhfunction{transl\_{3ac}} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$. However, instead we can define a relation \texttt{tr\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation. If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness. +To simplify the proof, instead of using the translation algorithm as an assumption, as was done in the backward simulation stated above, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness. For example, for the translation from 3AC to HTL, the translation might be defined using the following function: $\yhfunction{transl\_{3ac}} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$\NR{is the output HTL code?}. However, instead we can define a relation \texttt{tr\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation. If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness. \begin{equation*} \forall\ c\ h,\ \yhfunction{transl\_3ac} (c) = \yhconstant{OK}(h) \implies \yhfunction{tr\_htl}\ c\ h. |