data Instruction = Push Int | Inc | Pop | If Int | Store Int | Load Int | New String | Init String | Use String | Halt(The instructions
Jsr Int
and Ret Int
would
be considered extra credit.) The verification rules for each
instruction are in the
paper handed previously. The general strategy for the
implementation is described starting the bottom of page 144 of (or
section 4.9.2) The
Java Virtual Machine Specification, second edition. Step 4 on page
145 describes the simplest possible merging of values in which two
values which are not the same are merged to an unusable value. No need
to attempt to use sets of values like in the JBook.
data Instruction = Push Int | Inc | Pop | If Int -- Added April 11, 2003; should have been there all along | Store Int | Load Int | New String -- | Super String -- Deleted April 7, 2003 | Init String | Use String -- | Jsr String -- Replaced April 7, 2003; see next line | Jsr Int | Ret Int | Halt
(setq twelf-root "/l/twelf/") (load (concat twelf-root "emacs/twelf-init.el"))The documentation and examples are under the directory
/l/twelf
.