A Java Bytecode Formalisation
| Autor: | Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Computer science
Programming language 020207 software engineering Java bytecode 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Instruction set Bytecode 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Programming language specification 0202 electrical engineering electronic engineering information engineering Software_PROGRAMMINGLANGUAGES Java virtual machine computer Heap (data structure) computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030035914 VSTTE |
| DOI: | 10.1007/978-3-030-03592-1_8 |
| Popis: | This paper presents the first Coq formalisation of the full Java bytecode instruction set and its semantics. The set of instructions is organised in a hierarchy depending on how the instructions deal with the runtime structures of the Java Virtual Machine such as threads, stacks, heap etc. The hierarchical nature of Coq modules neatly reinforces this view and facilitates the understanding of the Java bytecode semantics. This approach makes it possible to both conduct verification of properties for programs and to prove metatheoretical results for the language. Based upon our formalisation experience, the deficiencies of the current informal bytecode language specification are discussed. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|