We present an initial link between Z and JML that has enabled us to use Z/Eves to prove theorems about JML classes. We have applied this to the JML type system and the java hashmap class from the java Collections Fram...
详细信息
ISBN:
(纸本)9783540752202
We present an initial link between Z and JML that has enabled us to use Z/Eves to prove theorems about JML classes. We have applied this to the JML type system and the java hashmap class from the java Collections Framework. We present and discuss the issues behind a more general strategy for translation in both directions between Z and JML. This work is a contribution to the Verified Software Repository, part of the Grand Challenge in Verified Software.
暂无评论