equal
deleted
inserted
replaced
28 @article{DvO-CPE01, |
28 @article{DvO-CPE01, |
29 author = {David von Oheimb}, |
29 author = {David von Oheimb}, |
30 title = {Hoare Logic for {J}ava in {Isabelle/HOL}}, |
30 title = {Hoare Logic for {J}ava in {Isabelle/HOL}}, |
31 journal = {Concurrency: Practice and Experience}, |
31 journal = {Concurrency: Practice and Experience}, |
32 year = {2001}, |
32 year = {2001}, |
|
33 volume = 598, |
|
34 pages = {??--??+43}, |
33 url = {http://www4.in.tum.de/papers/DvO-CPE01.html}, |
35 url = {http://www4.in.tum.de/papers/DvO-CPE01.html}, |
34 abstract = { |
36 abstract = { |
35 This article presents a Hoare-style calculus for a substantial subset |
37 This article presents a Hoare-style calculus for a substantial subset |
36 of Java Card, which we call Java_light. In particular, the language |
38 of Java Card, which we call Java_light. In particular, the language |
37 includes side-effecting expressions, mutual recursion, dynamic method |
39 includes side-effecting expressions, mutual recursion, dynamic method |