Next: Bibliography, Previous: JML to BML Compiler, Up: Top
See Mariela's document Java Bytecode Specification and Logic, in particular Sections 3 and 4 and 5 for a definition of a direct vcgen for bytecode (without using guarded commands), plus a correctness proof.