Changeset 580 for Deliverables


Ignore:
Timestamp:
Feb 18, 2011, 3:11:43 PM (9 years ago)
Author:
mulligan
Message:

Submitted version

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r579 r580  
    702702Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.
    703703
    704 We partially validated the assembly function by checking that on defined opcodes the \texttt{assembly\_1} and \texttt{fetch} functions are inverse.
     704We partially validated the assembler by checking that on defined opcodes the \texttt{assembly\_1} and \texttt{fetch} functions are inverse.
    705705
    706706The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.
Note: See TracChangeset for help on using the changeset viewer.