Search results

Create class DivisorNotZeroInvariant

model

prover

Status: Open.

#117 In team-worthwhile/worthwhile;

· bafain opened on Mar 10, 2012

Parse prover output for ProverResult to return AST model

feature

model

parser / validator / typesystem

prover

Status: Open.

#109 In team-worthwhile/worthwhile;

· bafain opened on Mar 3, 2012

Signal and display the assertion the prover is currently verifying

feature

prover

ui

Status: Open.

#97 In team-worthwhile/worthwhile;

· bafain opened on Feb 24, 2012

Formatter breaks syntactic correctness and modifies the program iteratively

ui

Status: Open.

#88 In team-worthwhile/worthwhile;

· jspam opened on Feb 21, 2012

When loop condition + invariant is verified, the whole loop is marked in the UI

prover

ui

Status: Open.

#74 In team-worthwhile/worthwhile;

· jspam opened on Feb 19, 2012

Pass validity prover output in annotationFailed/Succeeded methods

feature

interpreter

Status: Open.

#63 In team-worthwhile/worthwhile;

· jspam opened on Feb 17, 2012

Return value is not passed on to the prover in postconditions.

interpreter

Status: Open.

#61 In team-worthwhile/worthwhile;

· jspam opened on Feb 17, 2012

·  

Zwischenbericht Validierungsphase

Interpreter throws ugly error message when prover is missing

interpreter

Status: Open.

#58 In team-worthwhile/worthwhile;

· leonhandreke opened on Feb 17, 2012

·  

Kolloquium Validierungsphase

Improve `missing EOF at '_ensures'' syntax error

parser / validator / typesystem

Status: Open.

#36 In team-worthwhile/worthwhile;

· bafain opened on Feb 14, 2012

·  

Kolloquium Validierungsphase

Worthwhile reports Z3 timeout although Z3 is still running

prover

Status: Open.

#19 In team-worthwhile/worthwhile;

· tbormer opened on Feb 7, 2012