Commit b439d2ef authored by Alexander Weigl's avatar Alexander Weigl

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

parents 61e259a6 e6535e11
Pipeline #12007 failed with stage
in 1 minute and 27 seconds
......@@ -182,4 +182,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN);
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' )* ;
ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]')* ;
......@@ -36,6 +36,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
.put(Type.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
.put(Type.INT, VariableAssignments.VarType.INT)
.put(Type.STRING, VariableAssignments.VarType.OBJECT)
.put(Type.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
.build();
private static Logger logger = Logger.getLogger("interpreter");
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
......
public class Simple {
/*@ public invariant log != null && log.length == 100; @*/
public int[] log = new int[100];
/*@ public invariant n >= 0; @*/
public int n;
/*@ public normal_behavior
@ requires log != null;
@ ensures n == 0 && log != null;
@*/
public void init() {
for (int i = 0; i < log.length; i++) {
log[i] = 0;
}
n = 0;
}
/*@ public normal_behavior
@ requires n < 100;
@ ensures log[n] == x+y;
@ assignable log.*;
@*/
public void logging(int x, int y) {
if (n < 100) {
log[n] = x + y;
}
}
/*@ public normal_behavior
@ requires x >= 0 && y >= 0 && n <100;
@ ensures \result >=0;
@ assignable log.*;
@*/
public int example(int x, int y) {
if (log[n] == 0) {
logging(x, y);
return x + y;
} else {
return x + y;
}
}
/*@ public normal_behavior
@ requires a != null && b != null && (\forall int i; 0 <= i < a.length; a[i] != b[i]);
@ ensures (\forall int i; 0 <= i < a.length; a[i] != b[i]) && \old(a) == \result;
@*/
public int[] compare(int[] a, int[] b){
return a;
}
}
\ No newline at end of file
script t1(){
symbex;
cases{
case match `a[i] >= 0 ==> ` using[a:int[], i:int]:{
auto;
}
default{
auto;
}
}
}
script t(){
auto;
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment