In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution. The operational semantics are embedded into a $µ$-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions. Some examples of proving properties of programs using the embedding are presented. / I det här examensarbetet presenteras en operationell semantik för en delmängd av Javas virtuella maskin. Den delmängd som hanteras innehåller kontrollflöde, beräkningar och minneshantering. Vidare beskrivs semantiken för parallella exekveringstrådar. Den operationella semantiken formaliseras i en bevisassistent for $µ$-kalkyl, VeriCode Proof Tool (VCPT). VCPT har utvecklats vid Swedish Institiute of Computer Science (SICS), och har kraftfulla tekniker för att bevisa induktiva påståenden. Några exempel på bevis av egenskaper hos program användandes formaliseringen presenteras också.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-9512 |
| Date | January 2005 |
| Creators | Lagerkvist, Mikael Zayenz |
| Publisher | KTH, Elektronik- och datorsystem, ECS |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | IMIT/LECS ; 2005-70 |
Page generated in 0.0026 seconds