mattulbrich / dive Goto Github PK

4.0 5.0 0.0 69 MB

Dafny Interactive Verification Environment (DIVE)

License: GNU General Public License v3.0

SMT 0.12% Java 92.26% GAP 0.47% CSS 0.21% ANTLR 0.05% Shell 0.02% Roff 0.11% HTML 0.07% Dafny 2.03% Boogie 4.63% JavaScript 0.04%

dafny verification java

dive's People

Contributors

Stargazers

Watchers

dive's Issues

sophisticated Algorithm for unique parameter matching

The current algorithm to find a unique matching term for a given TermSelector is working but may lead to big machting terms pretty quickly. May there is a way to find smaller matching terms that are still unique.

DafnyException: Unknown class identifier

method getSum (a: int, b: int, c: int, d: int) returns (m: int)
    requires a > 0 && b > 0 && c > 0
    ensures m > 0
{
    var sum := a + b + c + d;
    m := sum;
}

and

method getMinMax(a: array<int>) returns (min: int, max: int)
  requires a != null
  requires a.Length >= 3
  requires forall i : int :: 1 <= i && i < a.Length-1 ==> a[i-1] != a[i] && a[i+1] != a[i]
  ensures forall i: int :: 0 <= i && i < a.Length ==> a[i] <= max
  ensures forall i: int :: 0 <= i && i < a.Length ==> a[i] >= min
  ensures max > min
{

  var one := a[0];
  var two := a[1];
  if (one > two)
  {
      max := one;
      min := two;
  } else {
      max := two;
      min := one;
  }
  var i: int := 1;
  while (i < a.Length)
    invariant 0 <= i && i <= a.Length
    invariant forall k: int :: 0 <= k && k < i ==> a[k] <= max
    invariant max > min
    invariant forall k: int :: 0 <= k && k < i ==> a[k] >= min
    decreases a.Length - i
  {
    if (a[i] > max)
    {
      max := a[i];
    }
    if (a[i] < min)
    {
        min := a[i];
    }
    i := i + 1;
  }
}

both result in the following exception:

/**
[java] Exception in Application start method
[java] java.lang.reflect.InvocationTargetException
[java] at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[java] at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[java] at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[java] at java.lang.reflect.Method.invoke(Method.java:498)
[java] at com.sun.javafx.application.LauncherImpl.launchApplicationWithArgs(LauncherImpl.java:389)
[java] at com.sun.javafx.application.LauncherImpl.launchApplication(LauncherImpl.java:328)
[java] at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[java] at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[java] at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[java] at java.lang.reflect.Method.invoke(Method.java:498)
[java] at sun.launcher.LauncherHelper$FXHelper.main(LauncherHelper.java:767)
[java] Caused by: java.lang.RuntimeException: Exception in Application start method
[java] at com.sun.javafx.application.LauncherImpl.launchApplication1(LauncherImpl.java:917)
[java] at com.sun.javafx.application.LauncherImpl.lambda$launchApplication$154(LauncherImpl.java:182)
[java] at java.lang.Thread.run(Thread.java:748)
[java] Caused by: edu.kit.iti.algover.parser.DafnyException: Unknown class identifier: a
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitID(ReferenceResolutionVisitor.java:196)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitID(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyDispatch.dispatch(DafnyDispatch.java:75)
[java] at edu.kit.iti.algover.parser.DafnyTree.accept(DafnyTree.java:349)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitDefault(ReferenceResolutionVisitor.java:173)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitDefault(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyTreeDefaultVisitor.visitARRAY_ACCESS(DafnyTreeDefaultVisitor.java:8)
[java] at edu.kit.iti.algover.parser.DafnyDispatch.dispatch(DafnyDispatch.java:15)
[java] at edu.kit.iti.algover.parser.DafnyTree.accept(DafnyTree.java:349)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitVAR(ReferenceResolutionVisitor.java:433)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitVAR(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyDispatch.dispatch(DafnyDispatch.java:169)
[java] at edu.kit.iti.algover.parser.DafnyTree.accept(DafnyTree.java:349)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitDefault(ReferenceResolutionVisitor.java:173)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitDefault(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyTreeDefaultVisitor.visitBLOCK(DafnyTreeDefaultVisitor.java:14)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitBLOCK(ReferenceResolutionVisitor.java:360)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitBLOCK(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyDispatch.dispatch(DafnyDispatch.java:27)
[java] at edu.kit.iti.algover.parser.DafnyTree.accept(DafnyTree.java:349)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitMETHOD(ReferenceResolutionVisitor.java:409)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitMETHOD(ReferenceResolutionVisitor.java:28)
[java] at edu.kit.iti.algover.parser.DafnyDispatch.dispatch(DafnyDispatch.java:111)
[java] at edu.kit.iti.algover.parser.DafnyTree.accept(DafnyTree.java:349)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitAll(ReferenceResolutionVisitor.java:155)
[java] at java.util.LinkedHashMap$LinkedValues.forEach(LinkedHashMap.java:608)
[java] at edu.kit.iti.algover.parser.ReferenceResolutionVisitor.visitProject(ReferenceResolutionVisitor.java:88)
[java] at edu.kit.iti.algover.project.ProjectBuilder.resolveNames(ProjectBuilder.java:271)
[java] at edu.kit.iti.algover.project.ProjectBuilder.build(ProjectBuilder.java:250)
[java] at edu.kit.iti.algover.project.ProjectManager.buildProject(ProjectManager.java:150)
[java] at edu.kit.iti.algover.project.ProjectManager.reload(ProjectManager.java:121)
[java] at edu.kit.iti.algover.project.ProjectManager.(ProjectManager.java:91)
[java] at edu.kit.iti.algover.AlgoVerApplication.start(AlgoVerApplication.java:41)
[java] at com.sun.javafx.application.LauncherImpl.lambda$launchApplication1$161(LauncherImpl.java:863)
[java] at com.sun.javafx.application.PlatformImpl.lambda$runAndWait$174(PlatformImpl.java:326)
[java] at com.sun.javafx.application.PlatformImpl.lambda$null$172(PlatformImpl.java:295)
[java] at java.security.AccessController.doPrivileged(Native Method)
[java] at com.sun.javafx.application.PlatformImpl.lambda$runLater$173(PlatformImpl.java:294)
[java] at com.sun.glass.ui.InvokeLaterDispatcher$Future.run(InvokeLaterDispatcher.java:95)
[java] at com.sun.glass.ui.win.WinApplication._runLoop(Native Method)
[java] at com.sun.glass.ui.win.WinApplication.lambda$null$147(WinApplication.java:177)
[java] ... 1 more
[java] Exception running application edu.kit.iti.algover.AlgoVerApplication

Dafny-Sets

Expressions like a: set<int> can be given as an argument to a function and are resolved just fine. However, set operations like e in b a * b a == {1,2,3} always throw exceptions. Will there be support for these in the future ? (Or is a special syntax required ?)

parse (and ignore) print statements

Est: 1h

Pretty printer for scripts

When a script has been expanded by mouse-click, the text layout should be revisited.

Interpreter not working after branching?

I have the suspicion that the interpreter does not work after branching rules. As an example open minSubArray and try the following script for the last pvc:

substitute on='let end := end_1 :: let start := start_1 :: let $decr_1 := 2 * |numArray| - end - start :: let end := end_2 :: let start := start_2 :: 0 <= 2 * |numArray| - end - start && 2 * |numArray| - end - start < $decr_1';
substitute on='let start := start_1 :: let $decr_1 := 2 * |numArray| - end_1 - start :: let end := end_2 :: let start := start_2 :: 0 <= 2 * |numArray| - end - start && 2 * |numArray| - end - start < $decr_1';
substitute on='let $decr_1 := 2 * |numArray| - end_1 - start_1 :: let end := end_2 :: let start := start_2 :: 0 <= 2 * |numArray| - end - start && 2 * |numArray| - end - start < $decr_1';
substitute on='let end := end_2 :: let start := start_2 :: 0 <= 2 * |numArray| - end - start && 2 * |numArray| - end - start < 2 * |numArray| - end_1 - start_1';
substitute on='let start := start_2 :: 0 <= 2 * |numArray| - end_2 - start && 2 * |numArray| - end_2 - start < 2 * |numArray| - end_1 - start_1';
substitute on='let end := end_1 :: end >= 0 && end <= |numArray|';
removeAssumption on='(forall k:int :: 0 <= k && k < |numArray| ==> $seq_get<int>(numArray, k) > 0)';
andRight on=' |- ... (?on: (0 <= 2 * |numArray| - end_2 - start_2 && 2 * |numArray| - end_2 - start_2 < 2 * |numArray| - end_1 - start_1 )) ...';
cases {
	case "case 1": {
	
	}
	case "case 2": {
	
substitute on='... (?on: (let start := start_1 :: start >= 0 && start <= |numArray| )) ... |- ';
	}
}

If i debug this both branches have 0 children after the interpretation which should not be the case. Any ideas?

Accessing fields of dafny-classes

The following simple example of using a class produces an exception:

`class Actor {
var x : int;
}

method getNumber (a : Actor) returns (m :int)
ensures m >= 0
{
if (a.x > 0) {
m:= 0;
} else {
m:= 1;
}
}
`

Exception in Application start method
java.lang.reflect.InvocationTargetException
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at com.sun.javafx.application.LauncherImpl.launchApplicationWithArgs(LauncherImpl.java:389)
at com.sun.javafx.application.LauncherImpl.launchApplication(LauncherImpl.java:328)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at sun.launcher.LauncherHelper$FXHelper.main(Unknown Source)
Caused by: java.lang.RuntimeException: Exception in Application start method
at com.sun.javafx.application.LauncherImpl.launchApplication1(LauncherImpl.java:917)
at com.sun.javafx.application.LauncherImpl.lambda$launchApplication$154(LauncherImpl.java:182)
at java.lang.Thread.run(Unknown Source)
Caused by: java.lang.Error: edu.kit.iti.algover.parser.DafnyException: edu.kit.iti.algover.term.builder.TermBuildException: Field x not found in class Actor
at edu.kit.iti.algover.proof.MethodPVCBuilder.ensureSequentExists(MethodPVCBuilder.java:147)
at edu.kit.iti.algover.proof.MethodPVCBuilder.getSequent(MethodPVCBuilder.java:153)
at edu.kit.iti.algover.proof.PVC.(PVC.java:85)
at edu.kit.iti.algover.proof.MethodPVCBuilder.build(MethodPVCBuilder.java:87)
at edu.kit.iti.algover.dafnystructures.DafnyDeclPVCCollector.visitMethod(DafnyDeclPVCCollector.java:69)
at edu.kit.iti.algover.dafnystructures.DafnyDeclPVCCollector.visitFile(DafnyDeclPVCCollector.java:104)
at edu.kit.iti.algover.project.Project.ensurePVCsExist(Project.java:302)
at edu.kit.iti.algover.project.Project.getPVCByNameMap(Project.java:321)
at edu.kit.iti.algover.project.ProjectManager.generateAllProofObjects(ProjectManager.java:174)
at edu.kit.iti.algover.project.ProjectManager.reload(ProjectManager.java:122)
at edu.kit.iti.algover.project.ProjectManager.(ProjectManager.java:91)
at edu.kit.iti.algover.AlgoVerApplication.start(AlgoVerApplication.java:41)
at com.sun.javafx.application.LauncherImpl.lambda$launchApplication1$161(LauncherImpl.java:863)
at com.sun.javafx.application.PlatformImpl.lambda$runAndWait$174(PlatformImpl.java:326)
at com.sun.javafx.application.PlatformImpl.lambda$null$172(PlatformImpl.java:295)
at java.security.AccessController.doPrivileged(Native Method)
at com.sun.javafx.application.PlatformImpl.lambda$runLater$173(PlatformImpl.java:294)
at com.sun.glass.ui.InvokeLaterDispatcher$Future.run(InvokeLaterDispatcher.java:95)
at com.sun.glass.ui.win.WinApplication._runLoop(Native Method)
at com.sun.glass.ui.win.WinApplication.lambda$null$147(WinApplication.java:177)
... 1 more
Caused by: edu.kit.iti.algover.parser.DafnyException: edu.kit.iti.algover.term.builder.TermBuildException: Field x not found in class Actor
at edu.kit.iti.algover.term.builder.UpdateSequenter.translate(UpdateSequenter.java:79)
at edu.kit.iti.algover.proof.MethodPVCBuilder.ensureSequentExists(MethodPVCBuilder.java:144)
... 20 more
Caused by: edu.kit.iti.algover.term.builder.TermBuildException: Field x not found in class Actor
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildFieldAccess(TreeTermTranslator.java:520)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.build(TreeTermTranslator.java:347)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildBinary(TreeTermTranslator.java:733)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.build(TreeTermTranslator.java:260)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildUnary(TreeTermTranslator.java:725)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.build(TreeTermTranslator.java:298)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildLetCascade(TreeTermTranslator.java:119)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildLetExpression(TreeTermTranslator.java:147)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.buildLetCascade(TreeTermTranslator.java:121)
at edu.kit.iti.algover.term.builder.TreeTermTranslator.build(TreeTermTranslator.java:113)
at edu.kit.iti.algover.term.builder.UpdateSequenter.translate(UpdateSequenter.java:74)
... 21 more
Exception running application edu.kit.iti.algover.AlgoVerApplication

algover parses a.Length instead of |a| where a is a sequence

correct Dafny syntax for the length of sequnces is |a| where a is the sequnce but algover expect a.Length which is not supported for sequnces

Support for method calls

method contracts must be used at call sites.

Support a < b < c

Dafny has built in support for continued inequalities. AlgoVer should parse this and transform it into a conjunction in a first transformation step.

Indeterminism of parsing of sequents (between gui and backend)

indeterminism concerning order of let clauses between gui and backend
example:
Taken from GUI: substitute on='(let max := max_1 :: (let i := i_1 :: $not($gt($array_select<int>($heap, a, i), max))))';
Now used in Backend: substitute on='(let i := i_1 :: (let max := max_1 :: $not($gt($array_select<int>($heap, a, i), max))))';

Support for functions

In early version, only methods have been considered.
Functions have their own issues:

Proof Verification Conditions also for functions
Reasoning about well-foundedness
Expanding function definitions

addReplecement for RuleApplicationBuilder only working in succedent

Replacements are only working in the succedent. Rather all replacements are applied to the succedent regardless of the polarity of the given TermSelector.

Example: i1 + i2 == 0 |- i3 == 0
replace ("A.0.0", i1)
results in i1 + i2 == 0 |- i1 == 0

Proposed fix:
change line 85 in RuleApplicator from
if (termSelectorTermPair.getFst().equals(TermSelector.SequentPolarity.ANTECEDENT)) {
to
if (termSelectorTermPair.getFst().isAntecedent()) {

and its working fine for me.

Support 'var i,j : int'

Dafny allows the declaration of more than one item per declaration.

Rule database

The fundamental rule database should support:

Propositional expansion
quantifier instantiation -> @matheus23 How does one provide the instantiation term in UI?
Rewrite lemmas in user files and libraries
cut -> Again: user instantiation
"this is the same as" -> UI
"cut on this"
apply equality
replace known left

pretty print Sequent view after rule application

the sequent view is filled with empty lines after a rule apllication. If you mouseover the view it changes to the pretty printed version (mainly removed empty lines). This should be done automatically not only on mouseover.

ProofFormulas are used for non-boolean terms

There are a number of test cases that create non-boolean proof formulas.
This is not admissible. An assertion has been added to check the sort of the formula.

Please fix the failing test cases by making the terms in proof formulas (boolean) formulas.

Use the branch fix71 for your fixes and merge it into master as soon as tests are fixed.
(starting at 8a57ff0)

Duplicate Formulas in Sequents

Discovered that there are cases where formulas are duplicates of each other in the sequent.

Support pretty printing for 'if c then a else b'

The parser supports this already.

PVCs for functions are not shown by the GUI

Since a8e6dd6, there are proof obligations also for the
well-formedness of function bodies.

They are shown and addresses in the CLI, but the GUI does not list the PVCs.

To reproduce, load modules/core/test-res/edu/kit/iti/algover/symbex/fib.dfy.

History Information Window

When selecting a formula F in the sequent view, the journal/logbook/proof ledger should be shown highlighting those ancient formulas which make up the history of F.

(@sgrebing suggests to have it in first milestone)

Reordering / Grouping / Collapsing of sequent formulas

When working with the UI, these steps help the user to structure her view on the proof. It's on the UI, not the models below

Support 'var i := 0'

If a variable is directly assigned, its type needs not be stated explicitly but can be inferred automatically.

Object Modification: PVC Generation

class X {
    var y: int;
}

method getNumber(o: X) 
    requires o != null
    ensures o.y > 5
    modifies o
{
    o.y := 8;
}

The generated proof verification conditions for ensures o.y > 5 do not seem to include the modifies clause and the method body. (Changing the order of ensures and modifies results in an immediate parsing exception)

support "new" constructions

mainly an issue for symbolic execution

new Class
new int[10]
field$created: field<Object,bool>

Exception while using the prover

While browsing (not applying rules!) the different proof obligations of the example sumAndMaxSeq, I obtained the following exception many times:

Exception in thread "JavaFX Application Thread" java.lang.ClassCastException: org.fxmisc.flowless.VirtualizedScrollPane cannot be cast to edu.kit.iti.algover.editor.DafnyCodeArea
	at edu.kit.iti.algover.editor.EditorController.lambda$viewReferences$2(EditorController.java:138)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.Iterator.forEachRemaining(Iterator.java:116)
	at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
	at java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
	at java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
	at java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:418)
	at edu.kit.iti.algover.editor.EditorController.viewReferences(EditorController.java:139)
	at edu.kit.iti.algover.MainController.onRequestReferenceHighlighting(MainController.java:140)
	at edu.kit.iti.algover.util.SubSelection.select(SubSelection.java:125)
	at edu.kit.iti.algover.util.SubSelection.lambda$subSelection$0(SubSelection.java:104)
	at edu.kit.iti.algover.util.SubSelection.select(SubSelection.java:125)
	at edu.kit.iti.algover.util.SubSelection.lambda$subSelection$0(SubSelection.java:104)
	at edu.kit.iti.algover.util.SubSelection.select(SubSelection.java:125)
	at edu.kit.iti.algover.sequent.OriginalFormulaView.handleClick(OriginalFormulaView.java:53)
	at com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:86)
	at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:238)
	at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:191)
	at com.sun.javafx.event.CompositeEventDispatcher.dispatchBubblingEvent(CompositeEventDispatcher.java:59)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
	at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
	at com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74)
	at com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:54)
	at javafx.event.Event.fireEvent(Event.java:198)
	at javafx.scene.Scene$MouseHandler.process(Scene.java:3757)
	at javafx.scene.Scene$MouseHandler.access$1500(Scene.java:3485)
	at javafx.scene.Scene.impl_processMouseEvent(Scene.java:1762)
	at javafx.scene.Scene$ScenePeerListener.mouseEvent(Scene.java:2494)
	at com.sun.javafx.tk.quantum.GlassViewEventHandler$MouseEventNotification.run(GlassViewEventHandler.java:394)
	at com.sun.javafx.tk.quantum.GlassViewEventHandler$MouseEventNotification.run(GlassViewEventHandler.java:295)
	at java.security.AccessController.doPrivileged(Native Method)
	at com.sun.javafx.tk.quantum.GlassViewEventHandler.lambda$handleMouseEvent$353(GlassViewEventHandler.java:432)
	at com.sun.javafx.tk.quantum.QuantumToolkit.runWithoutRenderLock(QuantumToolkit.java:389)
	at com.sun.javafx.tk.quantum.GlassViewEventHandler.handleMouseEvent(GlassViewEventHandler.java:431)
	at com.sun.glass.ui.View.handleMouseEvent(View.java:555)
	at com.sun.glass.ui.View.notifyMouse(View.java:937)
	at com.sun.glass.ui.gtk.GtkApplication._runLoop(Native Method)
	at com.sun.glass.ui.gtk.GtkApplication.lambda$null$48(GtkApplication.java:139)
	at java.lang.Thread.run(Thread.java:748)

Nullpointer when interpreting string regular expressions

A nullpointer exception occurs when evaluating a string match expression

Bug in Sequentmatcher

The following parameters for schemaSequent and concreteSequent return no match:

schemaSeq: ... let x := 5 :: x + 5 == 10 ...
concreteSeq: let x := 5 :: x + 5 == 10

i would expect something like ...0 => let x := 5 :: x + 5 == 10.

GUI fails if method does not have a contract

For a method like

method Main()
{
    // ...
    assert 1==1; // some assertion
}

I obtain the following exception in the GUI:

Exception in thread "JavaFX Application Thread" java.lang.IllegalStateException: It shouldn't be possible to not have any requires/ensures/decreases after method.
	at edu.kit.iti.algover.editor.PVCHighlightingRule.lambda$new$0(PVCHighlightingRule.java:74)
	at java.util.Optional.orElseThrow(Optional.java:290)
	at edu.kit.iti.algover.editor.PVCHighlightingRule.<init>(PVCHighlightingRule.java:74)
	at edu.kit.iti.algover.editor.EditorController.viewPVCSelection(EditorController.java:128)
	at edu.kit.iti.algover.MainController.onSelectBrowserItem(MainController.java:213)
	at edu.kit.iti.algover.browser.BrowserController.onTreeItemSelected(BrowserController.java:93)
	at com.sun.javafx.binding.ExpressionHelper$SingleChange.fireValueChangedEvent(ExpressionHelper.java:182)

on 8bde6dd

The example Problem1-SumMax is an example where this is needed.

GUI freezes when applying splitting rule

on 813375d863733a423038fb8c9e0ba91144aa8568.

To reproduce:

Load doc/examples/gcd
Choose PVC gcd/loop/else/Dec
In the succedent apply subst. exhaustively
Try to apply andRight in the succedent.

The GUI will freeze before the button even is released.

No modifies means modifies nothing

Unlike JML, Dafny assumes the empty write set if you do not specify any.

Currently a missing modifies is treated as modifies $everything

Shorten selection parameters in proof rule commands

When mouse-applied proof rules are brought into the script, it is desirable to not fully state all selected formulas, but to abbreviate. This makes the proof more robust against changes.

Implement abbreviation matching techniques
Implement auto-abbreviating mechanisms for proof saving

Bug in ProofNode construction on Interpretation

Since I merged in the master into my pk-fxgui branch, I can't interpret proofs anymore.

To investigate and make sure its not an issue with my GUI code I wrote a test (13c2799) and it is failing.

Did something change in the API? I'm basically only calling setScriptTextAndInterpret("subsitute ...") and then looking at the new ProofNode via proof.getProofRoot() and it has no children.

This is the test that fails:

    @Test
    public void missingProofNodeConstruction() throws Exception {
        // TODO: Maybe don't depend on doc/ directory, but instead on something inside test-res
        ProjectManager manager = new ProjectManager(new File("doc/examples/gcd/"), "config.xml");

        Proof proof = manager.getProofForPVC("gcd/InitInv.1");
        proof.setScriptTextAndInterpret("substitute on='(let $mod := $everything :: (let r := a :: (let x := b :: $gt(r, 0))))';");

        if (proof.getFailException() != null) {
            throw proof.getFailException();
        }

        assertEquals(1, proof.getProofRoot().getChildren().size());
    }

(it fails on the assertion, not the exception)

GUI broken

JavaFX GUI is pretty broken at the moment.

Commit

2a9459c (current master)

Reproduce

ant fxjar
java -jar algoverfx.jar
Choose sumAndMax
Try close all
Select any proof and Edit

Now the GUI is broken -- windows are empty, plenty of stack traces

Stacktrace

Bug in current matching algorithm for terms

Succedent:

let $mod := $everything ::
let r := a ::
let x := b ::
r > 0

Executing this script:

substitute on='(let x := b :: $gt(r, 0))';

Does not work, because it fails to find the given term on the succedent. (Basically in this line of code)

The terms arent equal, because of the interpretation of the "r" variable in both terms differs.
To the parser in the script the "r" seems to be a global constant, therefore is parsed as "ApplTerm" with 0 arity, while the original "r" in the succedent is bound by the LetTerm around it and is therefore a VariableTerm.

I don't know how to deal with this. It would be easy create another matching predicate (instead of using term::equals) that ignores differences between VariableTerms and ApplTerms, but that doesn't seem thought through and might lead to more successful matches than wanted.

Maybe this is also not that important to discuss anymore, since we have a new Matcher API soon, right? Its an interesting test case even for the new matcher, though, so I'm documenting it like this.

Allow lists of objects in modifies clauses

Currently, individual objects cannot be listed in a modifies clause.

The translation mechanism must be adapted that it accepts a list of objects and sets of objects.

var fp : set<object>;
// ...
modifies this, o, fp, {o}

Z3 translation

Working Z3 translation supporting the main concepts of the language

heap access
array access
quantifiers
let expressions

The Z3 connection should have:

result caching (see ivil)

Nice to have:

standing connection to Z3

bug in substitutionVisitor

Example:
considering following Term: let b3 := b1 :: let b1 := b2 :: b3
expected term after application of 2 let-substitutions: b2
actual term after both substitutions: b1

if im not mistaken the error occurs due to the fact that during the first substitution b3 gets replaced by b2 but b2 is not declared a variable term but a applicationterm and thus gets not replaced in the second substitution

decreases clauses are not supported

as stated above: the following code is valid but leads to an exeception when parsed:

while(end < |numArray|) 
      decreases |numArray| - end 
    {
       //some code
    }

Problems with accessing PVCs from Project

The PVC access mechanism seems to be broken.

I added two failing test cases to ProjectTest.

@sgrebing, can you please look into this?

parameters mapped to enum not .class

We disscussed tha the mapping of parameters from string to enum as (int, bool, term,...) would be cleaner.

support matching of multiple parameters in one matching expression

the idea came up that if there are more than one parameter and they are close to each other that maybe the user wants to use something like this:

randomRule params='... (?on : x) + (?with: x + 2)'

and thus match 2 parameters with only 1 matching expression.

support "new" constructions

mainly an issue for symbolic execution

new Class
new int[10]
~~field$created: field<Object,bool>~~

(generated from #20)

Feature Request: Warning if a case was not used at all

Issue a warning if one case does not apply to any goal.
The user should be notified because something is probably not as planned.

Impossible to deselect Term in SequentView

It is impossible to deselect a term once a term has been selected. This should be possible for example by clicking in an empty space in the ListView.

EmptyStackException when pretty-printing let

I got this Exception every time I wanted to pretty-print a let expression.

Exception in thread "JavaFX Application Thread" java.util.EmptyStackException
	at java.util.Stack.peek(Stack.java:102)
	at java.util.Stack.pop(Stack.java:84)
	at edu.kit.iti.algover.prettyprint.AnnotatedString.handlePopStyle(AnnotatedString.java:390)
	at edu.kit.iti.algover.prettyprint.LayoutMark$PopStyle.handle(LayoutMark.java:49)
	at edu.kit.iti.algover.prettyprint.AnnotatedString.mark(AnnotatedString.java:241)
	at de.uka.ilkd.pp.Printer.mark(Printer.java:122)
	at de.uka.ilkd.pp.Layouter.mark(Layouter.java:546)
	at edu.kit.iti.algover.prettyprint.PrettyPrintLayouter.resetPreviousStyle(PrettyPrintLayouter.java:94)
	at edu.kit.iti.algover.prettyprint.PrettyPrint.print(PrettyPrint.java:129)
	at edu.kit.iti.algover.prettyprint.PrettyPrint.print(PrettyPrint.java:104)
	at edu.kit.iti.algover.prettyprint.PrettyPrint.print(PrettyPrint.java:86)
	at edu.kit.iti.algover.OverviewController.onDoubleClickEntity(OverviewController.java:58)
        ...

The expression was generated from this file:

method x(x : int)
  ensures 1 == 1
{
  x := 1;
}

(I used the expression of the first succedent of this method's only PVC in my tests:

PrettyPrint print = new PrettyPrint();
print.setPrintingFix(false);
System.out.println(print.print(pvc.getSequent().getSuccedent().get(0).getTerm()));

)

I found a "fix": aa98201
but I don't know if that is the 'right' way to do it...

After "fixing", the pretty printer prints this expression: { x := 1 }$eq<int>(1, 1)

Support pretty printing and parsing of 'o.f @ heap'

Heap expressions need to be supported.

show changed Sequent after exhaustive rule application

after an exhaustive rule application via the GUI the sequent remains unchanged in the sequent view. Thus gives the impression the application didnt work. The user has to click into the script view and position the carrot at the end of the script to see the updated sequent. The default behaviour should be that the carrot is placed at the end of the script after each rule application und the sequent view should be updated accordingly.

bug display for number of closed pvcs

if the number of closed goals changes (e.g. you close a goal) the view is updated to display that but next to the function name in the browser view instaed of displaying the number of closed pvcs it appears to to be a open pvc itself

ScriptView on master is broken

It is not possible to switch nodes anymore in script view; Also no new Tabs are created when applying a branching rule.