The operational semantics of a Java Secure Processor
| Author(s) : | Moshe Levy Michael J. Butler Michael J. Butler Pieter H. Hartel Pieter H. Hartel Moshe Levy, |
| Publisher : | N/A |
| Publication Date : | 1998 |
| ISSN : | N/A |
| Abstract : | Abstract. A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors. 1, |