Ignore:
Timestamp:
Dec 14, 2010, 4:38:21 PM (9 years ago)
Author:
mulligan
Message:

Tweaks to the report.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r397 r422  
    124124The C compiler delivered by Work Package 3 will eventually produce machine code executable by our emulator, and we expect that the emulator will be useful as a debugging aid for the compiler writers.
    125125Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document.
    126 In particular, Deliverables D4.2 and D4.3 entail the implementation of a formalised version of the intermediate language of the compiler, along with an executable formal semantics of these languages.
    127 We expect our emulator will be of great use in the implementation of both of these deliverables for debugging and testing purposes.
     126Deliverables D4.2 and D4.3 entail the implementation of a formalised version of the intermediate language of the compiler, along with an executable formal semantics of these languages.
     127In particular, Deliverable D4.3 requires a formalisation of the semantics of the intermediate languages of the compiler, and Deliverable D4.4 requires a formal proof of the correspondence between the semantics of these formalized languages, and the formal semantics of the target processor.
     128The emulator(s) discussed in this report are the formalized semantics of our target processor made manifest.
    128129
    129130\section{A brief overview of the target processor}
     
    330331Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
    331332We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
    332 
    333 Further, we do not implement the pseudoinstructions present in the O'Caml emulator.
    334 The emulator accepts only `pure' 8051 assembly instructions.
    335333
    336334\subsection{Auxilliary data structures and libraries}
Note: See TracChangeset for help on using the changeset viewer.