Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
06ee58fb
Commit
06ee58fb
authored
May 31, 2017
by
Sarah Grebing
Browse files
Now with first version of contractchooser (atm does not deliver chosen contract yet)
parent
e5c867a9
Pipeline
#10888
failed with stage
in 1 minute and 55 seconds
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
pom.xml
View file @
06ee58fb
...
...
@@ -204,6 +204,13 @@
<artifactId>
guava
</artifactId>
<version>
22.0
</version>
</dependency>
<!-- https://mvnrepository.com/artifact/org.controlsfx/controlsfx -->
<dependency>
<groupId>
org.controlsfx
</groupId>
<artifactId>
controlsfx
</artifactId>
<version>
8.40.12
</version>
</dependency>
</dependencies>
...
...
src/main/java/edu/kit/formal/gui/controller/ContractChooser.java
0 → 100644
View file @
06ee58fb
package
edu.kit.formal.gui.controller
;
import
de.uka.ilkd.key.speclang.Contract
;
import
javafx.beans.property.SimpleListProperty
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.scene.control.ListView
;
import
org.controlsfx.dialog.WizardPane
;
/**
* WozardPane to dosplay all available contracts
*/
public
class
ContractChooser
extends
WizardPane
{
ListView
listOfContractsView
;
SimpleObjectProperty
<
Contract
>
chosen
;
public
ContractChooser
(
SimpleListProperty
<
Contract
>
contracts
,
Contract
chosenContract
)
{
initPane
();
listOfContractsView
.
itemsProperty
().
bind
(
contracts
);
this
.
chosen
.
bind
(
listOfContractsView
.
getSelectionModel
().
selectedItemProperty
());
}
private
void
initPane
()
{
this
.
setHeaderText
(
"KeY Contractchooser"
);
this
.
listOfContractsView
=
new
ListView
();
this
.
listOfContractsView
.
setVisible
(
true
);
this
.
setContent
(
listOfContractsView
);
this
.
setVisible
(
true
);
}
}
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
06ee58fb
package
edu.kit.formal.gui.controller
;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.gui.FileUtils
;
import
edu.kit.formal.gui.model.RootModel
;
import
edu.kit.formal.interpreter.KeYProofFacade
;
import
edu.kit.formal.interpreter.data.GoalNode
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.interpreter.dbg.Debugger
;
import
javafx.concurrent.Service
;
import
javafx.concurrent.Task
;
import
javafx.fxml.FXML
;
import
javafx.fxml.Initializable
;
import
javafx.scene.control.*
;
...
...
@@ -13,6 +16,7 @@ import javafx.scene.layout.Pane;
import
javafx.stage.FileChooser
;
import
javafx.stage.Stage
;
import
lombok.Setter
;
import
org.controlsfx.dialog.Wizard
;
import
java.io.File
;
import
java.net.URL
;
...
...
@@ -23,9 +27,13 @@ import java.util.concurrent.Executors;
/**
* Controller for the Debugger MainWindow
*
* @author S.Grebing
*/
public
class
DebuggerMainWindowController
implements
Initializable
{
private
static
String
testFile1
=
"/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/"
;
private
static
String
testFile
=
"/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/contraposition/"
;
@FXML
Pane
rootPane
;
...
...
@@ -62,8 +70,16 @@ public class DebuggerMainWindowController implements Initializable {
* **********************************************************************************************************/
@FXML
ListGoalView
goalView
;
ExecutorService
executorService
=
null
;
KeYProofFacade
facade
;
private
ExecutorService
executorService
=
null
;
private
KeYProofFacade
facade
;
private
Wizard
contractChooserDialog
=
new
Wizard
();
private
ContractLoaderService
cls
;
/**
* Model for the DebuggerController containing the neccessary references to objects needed for controlling backend through UI
...
...
@@ -105,7 +121,7 @@ public class DebuggerMainWindowController implements Initializable {
@FXML
protected
void
loadKeYFile
()
{
File
keyFile
=
openFileChooserDialog
(
"Select KeY File"
,
"KeY Files"
,
"key"
,
"java"
,
"script"
);
File
keyFile
=
openFileChooserDialog
(
"Select KeY File"
,
"KeY Files"
,
"key"
,
"script"
);
this
.
model
.
setKeYFile
(
keyFile
);
if
(
keyFile
!=
null
)
{
buildKeYProofFacade
();
...
...
@@ -114,6 +130,37 @@ public class DebuggerMainWindowController implements Initializable {
}
@FXML
protected
void
loadJavaFile
()
{
File
javaFile
=
openFileChooserDialog
(
"Select Java File"
,
"Java Files"
,
"java"
,
"script"
);
this
.
model
.
setJavaFile
(
javaFile
);
if
(
javaFile
!=
null
)
{
facade
=
new
KeYProofFacade
(
model
);
cls
.
setRefToRootModel
(
this
.
model
);
cls
.
start
();
cls
.
setOnSucceeded
(
event
->
{
model
.
getLoadedContracts
().
addAll
((
List
<
Contract
>)
event
.
getSource
().
getValue
());
contractChooserDialog
.
setFlow
(
new
Wizard
.
LinearFlow
(
new
ContractChooser
(
this
.
model
.
loadedContractsProperty
(),
this
.
model
.
getChosenContract
())));
contractChooserDialog
.
showAndWait
().
ifPresent
(
result
->
{
if
(
result
==
ButtonType
.
FINISH
)
{
System
.
out
.
println
(
"Wizard finished, loaded contracts: "
+
model
.
getChosenContract
());
}
});
});
/*
if (chosen != null) {
this.model.setChosenContract(chosen);
buildJavaProofFacade();
}*/
}
}
public
void
setStage
(
Stage
stage
)
{
this
.
stage
=
stage
;
}
...
...
@@ -121,6 +168,7 @@ public class DebuggerMainWindowController implements Initializable {
/**
* Needs to be set from calling method
*
* @param model
*/
public
void
setModel
(
RootModel
model
)
{
...
...
@@ -136,6 +184,8 @@ public class DebuggerMainWindowController implements Initializable {
scriptArea
.
init
();
goalView
.
setRootModel
(
this
.
model
);
goalView
.
init
();
// create and assign the flow
cls
=
new
ContractLoaderService
();
}
...
...
@@ -152,8 +202,21 @@ public class DebuggerMainWindowController implements Initializable {
executorService
=
Executors
.
newFixedThreadPool
(
2
);
executorService
.
execute
(()
->
{
facade
=
new
KeYProofFacade
(
model
);
facade
.
buildKeYInterpreter
(
model
.
getKeYFile
());
facade
.
prepareEnvWithKeYFile
(
model
.
getKeYFile
());
});
executorService
.
shutdown
();
}
/**
* Spawns a thread that builds the proof environment as facade with interpreter
*/
private
void
buildJavaProofFacade
()
{
executorService
=
Executors
.
newFixedThreadPool
(
2
);
executorService
.
execute
(()
->
{
if
(
facade
!=
null
)
{
facade
.
prepareEnvForContract
(
model
.
getChosenContract
(),
model
.
getKeYFile
());
}
});
executorService
.
shutdown
();
}
...
...
@@ -171,11 +234,35 @@ public class DebuggerMainWindowController implements Initializable {
FileChooser
fileChooser
=
new
FileChooser
();
fileChooser
.
setTitle
(
title
);
fileChooser
.
setSelectedExtensionFilter
(
new
FileChooser
.
ExtensionFilter
(
description
,
fileEndings
));
fileChooser
.
setInitialDirectory
(
new
File
(
"/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/contraposition/"
));
fileChooser
.
setInitialDirectory
(
new
File
(
testFile1
));
File
file
=
fileChooser
.
showOpenDialog
(
this
.
stage
);
return
file
;
}
public
class
ContractLoaderService
extends
Service
<
List
<
Contract
>>
{
@Setter
RootModel
refToRootModel
;
@Override
protected
Task
<
List
<
Contract
>>
createTask
()
{
Task
<
List
<
Contract
>>
task1
=
new
Task
<
List
<
Contract
>>()
{
@Override
protected
List
<
Contract
>
call
()
throws
Exception
{
if
(
refToRootModel
!=
null
)
{
List
<
Contract
>
contracts
=
facade
.
getContractsForJavaFile
(
refToRootModel
.
getJavaFile
());
System
.
out
.
println
(
"Loaded Contracts "
+
contracts
.
toString
());
return
contracts
;
}
else
{
throw
new
RuntimeException
(
"No Reference to Rootmodel"
);
}
}
};
System
.
out
.
println
(
"Task1 created"
);
return
task1
;
}
}
}
src/main/java/edu/kit/formal/gui/model/RootModel.java
View file @
06ee58fb
package
edu.kit.formal.gui.model
;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.interpreter.data.GoalNode
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.interpreter.data.State
;
...
...
@@ -24,6 +25,11 @@ public class RootModel {
*/
private
final
SimpleObjectProperty
<
File
>
scriptFile
;
/**
* Property: current loaded javaFile
*/
private
final
SimpleObjectProperty
<
File
>
javaFile
;
/**
* Property: current loaded KeY File
*/
...
...
@@ -44,17 +50,25 @@ public class RootModel {
*/
private
SimpleObjectProperty
<
GoalNode
<
KeyData
>>
currentSelectedGoalNode
;
private
SimpleListProperty
<
Contract
>
loadedContracts
;
private
Contract
chosenContract
;
@Getter
@Setter
private
State
<
KeyData
>
currentState
;
public
RootModel
()
{
javaFile
=
new
SimpleObjectProperty
<>();
scriptFile
=
new
SimpleObjectProperty
<>();
keYFile
=
new
SimpleObjectProperty
<>();
currentScript
=
new
SimpleObjectProperty
<>(
""
);
currentSelectedGoalNode
=
new
SimpleObjectProperty
<>();
currentGoalNodes
=
new
SimpleListProperty
<>(
FXCollections
.
observableArrayList
());
loadedContracts
=
new
SimpleListProperty
<>(
FXCollections
.
observableArrayList
());
}
...
...
@@ -122,6 +136,38 @@ public class RootModel {
return
currentSelectedGoalNode
;
}
public
File
getJavaFile
()
{
return
javaFile
.
get
();
}
public
void
setJavaFile
(
File
javaFile
)
{
this
.
javaFile
.
set
(
javaFile
);
}
public
SimpleObjectProperty
<
File
>
javaFileProperty
()
{
return
javaFile
;
}
public
ObservableList
<
Contract
>
getLoadedContracts
()
{
return
loadedContracts
.
get
();
}
public
void
setLoadedContracts
(
ObservableList
<
Contract
>
loadedContracts
)
{
this
.
loadedContracts
.
set
(
loadedContracts
);
}
public
SimpleListProperty
<
Contract
>
loadedContractsProperty
()
{
return
loadedContracts
;
}
public
Contract
getChosenContract
()
{
return
chosenContract
;
}
public
void
setChosenContract
(
Contract
chosenContract
)
{
this
.
chosenContract
=
chosenContract
;
}
...
...
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
View file @
06ee58fb
...
...
@@ -4,7 +4,9 @@ import de.uka.ilkd.key.api.KeYApi;
import
de.uka.ilkd.key.api.ProjectedNode
;
import
de.uka.ilkd.key.api.ProofApi
;
import
de.uka.ilkd.key.api.ProofManagementApi
;
import
de.uka.ilkd.key.proof.init.ProofInputException
;
import
de.uka.ilkd.key.proof.io.ProblemLoaderException
;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.gui.model.RootModel
;
import
edu.kit.formal.interpreter.data.GoalNode
;
import
edu.kit.formal.interpreter.data.KeyData
;
...
...
@@ -15,6 +17,7 @@ import lombok.Getter;
import
java.io.File
;
import
java.io.IOException
;
import
java.util.List
;
/**
* Created by sarah on 5/29/17.
...
...
@@ -39,7 +42,7 @@ public class KeYProofFacade {
}
public
State
<
KeyData
>
executeScriptWithKeYProblemFile
(
String
currentScriptText
,
File
keyProblemFile
)
{
buildKeYInterpreter
(
keyProblemFile
);
buildKeYInterpreter
(
keyProblemFile
,
false
);
currentRoot
=
pa
.
getFirstOpenGoal
();
KeyData
keyData
=
new
KeyData
(
currentRoot
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
...
...
@@ -53,24 +56,50 @@ public class KeYProofFacade {
}
public
void
prepareEnvWithKeYFile
(
File
keYFile
)
{
try
{
pma
=
KeYApi
.
loadFromKeyFile
(
keYFile
);
pa
=
pma
.
getLoadedProof
();
buildKeYInterpreter
(
keYFile
,
false
);
}
catch
(
ProblemLoaderException
e
)
{
e
.
printStackTrace
();
}
}
public
List
<
Contract
>
getContractsForJavaFile
(
File
javaFile
)
{
try
{
pma
=
KeYApi
.
loadFromKeyFile
(
javaFile
);
return
pma
.
getProofContracts
();
}
catch
(
ProblemLoaderException
e
)
{
e
.
printStackTrace
();
}
return
null
;
}
public
void
prepareEnvForContract
(
Contract
c
,
File
javaFile
)
{
try
{
pa
=
pma
.
startProof
(
c
);
buildKeYInterpreter
(
javaFile
,
true
);
}
catch
(
ProofInputException
e
)
{
e
.
printStackTrace
();
}
}
/**
* Build the KeYInterpreter that handles the execution of the loaded key problem file
*
* @param keYFile
*/
p
ublic
void
buildKeYInterpreter
(
File
keYFile
)
{
p
rivate
void
buildKeYInterpreter
(
File
keYFile
,
Boolean
isJavaFile
)
{
InterpreterBuilder
interpreterBuilder
=
new
InterpreterBuilder
();
this
.
interpreter
=
null
;
try
{
pma
=
KeYApi
.
loadFromKeyFile
(
keYFile
);
pa
=
pma
.
getLoadedProof
();
interpreterBuilder
.
proof
(
pa
).
macros
().
scriptCommands
();
pa
.
getProof
().
getProofIndependentSettings
().
getGeneralSettings
().
setOneStepSimplification
(
false
);
this
.
interpreter
=
interpreterBuilder
.
build
();
interpreterBuilder
.
proof
(
pa
).
macros
().
scriptCommands
();
pa
.
getProof
().
getProofIndependentSettings
().
getGeneralSettings
().
setOneStepSimplification
(
false
);
this
.
interpreter
=
interpreterBuilder
.
build
();
}
catch
(
ProblemLoaderException
e
)
{
e
.
printStackTrace
();
}
}
...
...
src/main/resources/DebuggerMain.fxml
View file @
06ee58fb
...
...
@@ -62,6 +62,9 @@
text=
"Open Script"
/>
<MenuItem
fx:id=
"loadKeYFileMenuItem"
mnemonicParsing=
"false"
onAction=
"#loadKeYFile"
text=
"Load KeY File"
/>
<MenuItem
fx:id=
"loadJavaFileMenuItem"
mnemonicParsing=
"false"
onAction=
"#loadJavaFile"
text=
"Load Java File"
/>
<MenuItem
fx:id=
"closeMenuItem"
mnemonicParsing=
"false"
onAction=
"#closeProgram"
text=
"Close"
/>
</items>
</Menu>
...
...
src/test/resources/edu/kit/formal/interpreter/javaExample/TwoWaySwap.java
0 → 100644
View file @
06ee58fb
public
class
TwoWaySwap
{
private
boolean
[]
a
;
//@ model \seq seq;
//@ represents seq = \dl_array2seq(a);
/*@ public normal_behavior
@ ensures a == _a;
@ modifies a;
@*/
public
void
set
(
boolean
[]
_a
)
{
a
=
_a
;
}
/*@ public normal_behavior
@ requires i >= 0 && i<a.length && j >= 0 && j<a.length;
@ ensures a[i] == \old(a[j]) && a[j] == \old(a[i]);
@ ensures seq == \dl_seqSwap(\old(seq), i, j);
@ assignable a[i], a[j];
@*/
public
void
swap
(
int
i
,
int
j
)
{
boolean
t
=
a
[
i
];
a
[
i
]
=
a
[
j
];
a
[
j
]
=
t
;
}
/*@ public normal_behavior
@ ensures (\forall int k;
@ (\forall int l; k>=0 && k < l && l<a.length; a[k] == a[l] || !a[k]));
@ ensures \dl_seqPerm(\old(seq), seq);
@ assignable a[*];
@*/
public
void
twoWaySort
()
{
int
i
=
0
;
int
j
=
a
.
length
-
1
;
/*@ loop_invariant
@ i>=0 && j < a.length && j-i >= -1 &&
@ (\forall int m; m>=0 && m<i; !a[m]) &&
@ (\forall int m; m>j && m<a.length; a[m]) &&
@ (\forall int m; m>=i && m <=j; a[m] == \old(a[m])) &&
@ \dl_seqPerm(\old(seq), seq);
@ assignable a[*];
@ decreases j - i + 1;
@*/
while
(
i
<=
j
)
{
if
(!
a
[
i
])
{
i
=
i
+
1
;
}
else
if
(
a
[
j
])
{
j
=
j
-
1
;
}
else
{
swap
(
i
,
j
);
i
=
i
+
1
;
j
=
j
-
1
;
}
}
}
}
\ No newline at end of file
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment