|
|
|---|
|
|
|
|---|
Executable refinements of the execution functions.
In the specification, the only functions that depend on decode are step and stepn; the instruction semantic functions do not depend on decoding, because they operate on the instruction abstract syntax produced by decoding. Here we provide executable versions stepx and stepnx of step and stepn, by propagating the refinement of decode to decodex via the apt::simplify transformation.