Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
Refute: refuting (case 4)
The refute statement is reachable, therefore it is valid.
General Information
Backend
: Chalice
Language
: Java
Features
:
Path to Example File
: refute/refute4.java
Should Verify
: Yes
Date
: 2017-06-20
Lines of Code
: 14 (comments not included)
Lines of Specification
: 5 (35.7% of total)
Computation Time
: 16.8 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases Refute4 //:: tools silicon //:: verdict Pass /* The refute statement is reachable, therefore it is valid. */ public class Refute { int x; /*@ requires Perm(x,write) ** x==2; ensures Perm(x,write) ** x==3; @*/ public void good2(){ //@ refute x==3; x = 3; } }
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper