# Changeset 2370

Ignore:
Timestamp:
Sep 28, 2012, 4:19:25 PM (7 years ago)
Message:

Added reference to Jaap's ArXiv? paper

Location:
Papers/cpp-asm-2012
Files:
2 edited

### Legend:

Unmodified
 r2369 \label{subsect.total.correctness.for.well.behaved.assembly.programs} The traditional approach to verifying the correctness of an assembler is to restrict the semantics of assembly code to treat memory addresses as opaque (symbolic) structures that cannot be modified. Memory is represented as a map from opaque addresses to the disjoint union of data and opaque addresses---addresses are kept opaque to prevent their possible semantics breaking' manipulation by assembly programs: The traditional approach to verifying the correctness of an assembler is to restrict the semantics of assembly code so that it treats memory addresses as opaque (symbolic) structures that cannot be modified. Memory is then represented as a map from opaque addresses to the disjoint union of data and opaque addresses---addresses are kept opaque to prevent their possible semantics breaking' manipulation by assembly programs: \begin{displaymath} \mathtt{Mem} : \mathtt{Addr} \rightarrow \mathtt{Bytes} + \mathtt{Addr} \qquad \llbracket - \rrbracket : \mathtt{Instr} \rightarrow \mathtt{Mem} \rightarrow \mathtt{option\ Mem}