Commit fe2d7fa5 authored by LULUDBR\Lulu's avatar LULUDBR\Lulu

Sortskript of Quicksort

parent a7a11606
Pipeline #17054 passed with stages
in 9 minutes and 12 seconds
...@@ -46,6 +46,40 @@ cases{ ...@@ -46,6 +46,40 @@ cases{
} }
}
script sort() {
autopilot_prep;
foreach{
simp_upd;
tryclose;
}
// one open goal in der Bedingung: if(from < to) -> Post (split) -> Post (sort) ->
seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)),length(array), any::select(heapAfter_split, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))))`;
seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))))`;
auto;
} }
script shorter(){ script shorter(){
......
...@@ -12,7 +12,8 @@ ...@@ -12,7 +12,8 @@
<?import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView?> <?import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView?>
<?import edu.kit.iti.formal.psdbg.gui.controls.SectionPane?> <?import edu.kit.iti.formal.psdbg.gui.controls.SectionPane?>
<?import javafx.scene.layout.Pane?> <?import javafx.scene.layout.Pane?>
<?import edu.kit.iti.formal.psdbg.gui.controls.SequentView?> <?import edu.kit.iti.formal.psdbg.gui.controls.SequentViewForMatcher?>
<fx:root xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1" <fx:root xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1"
type="edu.kit.iti.formal.psdbg.gui.controls.SequentMatcher"> type="edu.kit.iti.formal.psdbg.gui.controls.SequentMatcher">
<center> <center>
...@@ -35,7 +36,7 @@ ...@@ -35,7 +36,7 @@
<SectionPane title="Sequent" minHeight="0.0" minWidth="0.0" prefHeight="633.0" <SectionPane title="Sequent" minHeight="0.0" minWidth="0.0" prefHeight="633.0"
prefWidth="341.0"> prefWidth="341.0">
<center> <center>
<SequentView fx:id="sequentView"/> <SequentViewForMatcher fx:id="sequentView"/>
</center> </center>
</SectionPane> </SectionPane>
<SplitPane dividerPositions="0.28551136363636365" layoutX="11.0" layoutY="12.0" <SplitPane dividerPositions="0.28551136363636365" layoutX="11.0" layoutY="12.0"
......
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