Published February 11, 2022
| Version 1.0
Journal article
Open
Reasoning About Invariant Properties of Object-oriented Programs-dynamic frames: Proof files
Creators
Description
The project files for the article `Reasoning About Invariant Properties of Object-oriented Programs' . This file is for the dynamic frames approach. The archive contains:
- The bundled version of KeY, key-2.8.0-exe.jar.
- The java source code of the project.
- User-defined taclets that we need when we do the proof (DynamicFrame_rule.key)
- Proof files for our case study(block contract that contains assignable clause and operation contract for reachability predicate).
- The related video: https://doi.org/10.6084/m9.figshare.16782667.v1
Files
Reasoning About Invariant Properties of Object-oriented Programs.zip
Files
(24.7 MB)
Name | Size | Download all |
---|---|---|
md5:691a03340dd911886780926d95163247
|
24.7 MB | Preview Download |