Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
History-based reasoning: correctness checking (Java)
Verification example in Java where there correctness of defined processes and axioms is verified.
General Information
Backend
: Silicon
Language
: Java
Features
: Histories
Path to Example File
: histories/HistoryJava.java
Should Verify
: Yes
Date
: 2017-06-19
Lines of Code
: 33 (comments not included)
Lines of Specification
: 16 (48.5% of total)
Computation Time
: 25.6 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases HistoryApplication class History { int x; /*@ modifies x; ensures x==\old(x)+1; process incr(); modifies x; requires n>=0; ensures x==\old(x)+n; process single(int n)=n>0?incr()*single(n-1):empty; modifies x; requires n>=0 && m >= 0; ensures x==\old(x)+n+m; process dual(int n,int m)=single(n)||single(m); requires n >= 0 ; ensures single(n)==(n>0?single(n-1)*incr():empty); ghost void lemma(int n); requires m>=0 && n >= 0 ; ensures single(m)*single(n)==single(m+n); ghost void single_axiom(int m,int n); @*/ }
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper