janhaag/PSE2011 — Issue #80: Division by zero in bounded quantified expression
Author: ratefuchs
Created: 2012-03-03 19:58:47+00:00
State: open
Labels: Interpreter

When interpreting the following program:

main() {}ensure exists x(-1,0) 1/x==1;

the program stops executing but thinks it is executing (so several things cannot be changed) and a stacktrace printed on the IDE console:

Exception in thread "Thread-0" java.lang.ArithmeticException: BigInteger divide by zero
at java.math.MutableBigInteger.divide(MutableBigInteger.java:869)
at java.math.BigInteger.divide(BigInteger.java:1314)
at interpreter.Interpreter.divide(Interpreter.java:148)
at interpreter.Interpreter.visit(Interpreter.java:131)
at ast.ArithmeticExpression.accept(ArithmeticExpression.java:70)
at interpreter.Interpreter.visit(Interpreter.java:164)
at ast.LogicalExpression.accept(LogicalExpression.java:69)
at interpreter.Interpreter.visit(Interpreter.java:168)
at ast.LogicalExpression.accept(LogicalExpression.java:69)
at interpreter.Interpreter.visit(Interpreter.java:439)
at ast.ExistsQuantifier.accept(ExistsQuantifier.java:25)
at interpreter.Interpreter.visit(Interpreter.java:378)
at ast.Ensure.accept(Ensure.java:21)
at interpreter.Interpreter.adjustStatement(Interpreter.java:495)
at interpreter.Interpreter.visit(Interpreter.java:359)
at ast.Assertion.accept(Assertion.java:22)
at interpreter.Interpreter.step(Interpreter.java:40)
at misc.ExecutionHandler.singleStep(ExecutionHandler.java:106)
at misc.ExecutionHandler.run(ExecutionHandler.java:80)
at gui.controller.MainController$1.run(MainController.java:247)