Piton pp 97-130 | Cite as

The Implementation of Piton on FM9001

Part of the Automated Reasoning Series book series (ARSE, volume 3)


To implement Piton on FM9001 we define ‘load’. ‘Load’ takes a p-state, a list of natural numbers, boot-lst, and a load address, load-addr, as its input and produces an FM9001 state as its output. ‘Load’ carries out four successive transformations starting with the initial p-state and ending with an FM9001 state. Each such transformation is described by a function and ‘load’ is the composition of those four functions. The four functions have names that suggest they are transforms from one state space to another. For example, the function ‘p⇒r’ transforms p-states to what we call “r-states.” We explain these intermediate forms later.


Data Segment Program Counter Assembly Code Machine Code FM9001 State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Kluwer Academic Publishers 1996

Personalised recommendations