Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add code from report #16

Merged
merged 13 commits into from
Apr 29, 2024
Merged

Add code from report #16

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
9fc3ba7
Copy over files
dnezam Apr 13, 2024
24c77d7
Remove configured values
dnezam Apr 13, 2024
0445f77
Add license information
dnezam Apr 13, 2024
10565b0
Add information about Z3 version
dnezam Apr 13, 2024
6561df8
Rename folder
dnezam Apr 13, 2024
b321539
Add usage and dependencies as comment
dnezam Apr 13, 2024
ba80f9d
Add missing noaxioms_sets.vpr
dnezam Apr 13, 2024
f0c1f1b
Use env vars for profile-all.sh
dnezam Apr 25, 2024
da69ed5
Add titles to used_commands.md
dnezam Apr 25, 2024
a9adec7
Add README.md for evaluation/
dnezam Apr 25, 2024
3a0515d
Fix link in evaluation/README.md
dnezam Apr 25, 2024
95781f5
Use python3 + Extend README
dnezam Apr 26, 2024
e6b5c5e
Make profile-all.sh executable
dnezam Apr 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions ...t_half/first_half-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
qi-k!542,qi-k!553,qi-k!587,qi-k!565,qi-quant-u-8,qi-quant-u-9,qi-$Multiset[Int]_prog.card_non_negative,qi-$Multiset[Int]_prog.card_empty,qi-quant-u-27,qi-quant-u-2,qi-quant-u-26,qi-quant-u-3,qi-quant-u-0,qi-quant-u-24,qi-quant-u-1,qi-quant-u-10,qi-quant-u-11,qi-quant-u-35,qi-quant-u-34,qi-quant-u-4,qi-quant-u-28,qi-quant-u-5,qi-quant-u-43,qi-quant-u-18,qi-quant-u-42,qi-quant-u-19,qi-quant-u-33,qi-quant-u-32,qi-quant-u-41,qi-quant-u-16,qi-quant-u-40,qi-quant-u-17,qi-quant-u-6,qi-quant-u-30,qi-quant-u-7,qi-quant-u-12,qi-quant-u-36,qi-quant-u-13,qi-$Multiset[Int]_prog.count_card,qi-$Multiset[Int]_prog.singleton_unionone,qi-$Multiset[Int]_prog.card_union,qi-$Multiset[Int]_prog.count_union,qi-$Multiset[Int]_prog.card_unionone,qi-$Multiset[Int]_prog.count_singleton,qi-$Multiset[Int]_prog.count_unionone,qi-$Multiset[Int]_prog.count_empty,qi-quant-u-14,qi-quant-u-38,qi-quant-u-15,qi-$Multiset[Int]_prog.equal_count,qi-quant-u-22,qi-quant-u-45,qi-quant-u-23,qi-quant-u-44,qi-$Multiset[Int]_prog.native_equality,qi-prog.getter_over_tuple2,qi-quant-u-20,qi-quant-u-21,qi-prog.integer_ax_dec,qi-k!569,qi-k!593,qi-k!599,qi-prog.integer_ax_bound,execution_time
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.57454514503479
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.84791350364685
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.858602523803711
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.771847009658813
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.01976990699768
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.935436010360718
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.75414776802063
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.120795011520386
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.82166314125061
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.02254605293274
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.238065481185913
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.151848554611206
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.836472272872925
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.892492055892944
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.741572380065918
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.007696628570557
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.838359117507935
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.95261025428772
1,62,45,25,13,32,85,85,31,30,31,52,30,30,30,7,17,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,192,13,27,52,13,45,45,15,1,1,1,12,1,1,1,1,1,3,2,1,9,82,44,44,6,10.821515798568726
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.83070993423462
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.751307964324951
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.833659172058105
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.8695068359375
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.117118120193481
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.845272064208984
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.208571195602417
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.688027620315552
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.872260570526123
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.039685249328613
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.644623517990112
Binary file added ...er_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.execution_time.png
View file
Open in desktop
dnezam marked this conversation as resolved.
Show resolved Hide resolved
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ...half-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.qi.png
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
104 changes: 104 additions & 0 deletions evaluation/experiments/program_proofs_example_10_2/first_half/first_half.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
// This package contains the first half of the proof for InsertCorrect from
// https://github.com/viperproject/program-proofs-gobra/blob/main/chapter10/examples_10.2.gobra
package first_half

ghost
requires pq.Valid()
ensures let pqPrime := pq.Insert(y) in
pqPrime.Valid() &&
pqPrime.Elements() == pq.Elements() union mset[int]{y}
decreases len(pq)
pure func (pq PQueue) InsertCorrect(y int) Unit {
return match pq {
case Leaf{}:
Unit{}
case Node{?x, ?l, ?r}:
let pqPrime := pq.Insert(y) in
let min := y < x ? y : x in
let max := y < x ? x : y in
let newRight := r.Insert(max) in
let _ := asserting(pqPrime == Node{min, newRight, l}) in
let _ := asserting(
let L := len(l.Elements()) in
let R := len(r.Elements()) in
L == R || L == R + 1) in
r.InsertCorrect(max)
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Valid() bool {
return pq.IsBinaryHeap() && pq.IsBalanced()
}

ghost
decreases len(pq)
pure func (pq PQueue) Insert(y int) PQueue {
return match pq {
case Leaf{}:
Node{y, Leaf{}, Leaf{}}
case Node{?x, ?left, ?right}:
y < x ? Node{y, right.Insert(x), left} : Node{x, right.Insert(y), left}
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Elements() mset[int] {
return match pq {
case Leaf{}:
mset[int]{}
case Node{?x, ?left, ?right}:
mset[int]{x} union left.Elements() union right.Elements()
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBalanced() (res bool) {
return match pq {
case Leaf{}:
true
case Node{_, ?left, ?right}:
left.IsBalanced() && right.IsBalanced() &&
(let L := len(left.Elements()) in
let R := len(right.Elements()) in
L == R || L == R + 1)
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBinaryHeap() bool {
return match pq {
case Leaf{}:
true
case Node{?x, ?left, ?right}:
left.IsBinaryHeap() && right.IsBinaryHeap() &&
(left == Leaf{} || x <= left.x) &&
(right == Leaf{} || x <= right.x)
}
}


type Unit struct{}

ghost
requires b
decreases
pure func asserting(b bool) Unit {
return Unit{}
}

type PQueue = BraunTree

type BraunTree adt {
Leaf {}

Node {
x int
left BraunTree
right BraunTree
}
}
31 changes: 31 additions & 0 deletions ...le_10_2/full/full-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
qi-k!601,qi-k!544,qi-k!578,qi-k!556,qi-quant-u-8,qi-quant-u-9,qi-$Multiset[Int]_prog.card_non_negative,qi-$Multiset[Int]_prog.card_empty,qi-quant-u-27,qi-quant-u-2,qi-quant-u-26,qi-quant-u-3,qi-quant-u-0,qi-quant-u-24,qi-quant-u-1,qi-quant-u-10,qi-quant-u-11,qi-quant-u-35,qi-quant-u-34,qi-quant-u-4,qi-quant-u-28,qi-quant-u-5,qi-quant-u-43,qi-quant-u-18,qi-quant-u-42,qi-quant-u-19,qi-quant-u-33,qi-quant-u-32,qi-quant-u-41,qi-quant-u-16,qi-quant-u-40,qi-quant-u-17,qi-quant-u-6,qi-quant-u-30,qi-quant-u-7,qi-quant-u-12,qi-quant-u-36,qi-quant-u-13,qi-$Multiset[Int]_prog.count_card,qi-$Multiset[Int]_prog.singleton_unionone,qi-$Multiset[Int]_prog.card_union,qi-$Multiset[Int]_prog.count_union,qi-$Multiset[Int]_prog.card_unionone,qi-$Multiset[Int]_prog.count_singleton,qi-$Multiset[Int]_prog.count_unionone,qi-$Multiset[Int]_prog.count_empty,qi-quant-u-22,qi-quant-u-45,qi-quant-u-23,qi-quant-u-44,qi-$Multiset[Int]_prog.equal_count,qi-$Multiset[Int]_prog.native_equality,qi-quant-u-14,qi-quant-u-38,qi-quant-u-15,qi-prog.getter_over_tuple2,qi-quant-u-20,qi-quant-u-21,qi-prog.integer_ax_dec,qi-k!560,qi-k!584,qi-k!590,qi-prog.integer_ax_bound,qi-quant-u-47,qi-quant-u-46,execution_time
1,73,56,17,18,41,110,110,44,43,44,53,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,178,17,44,69,22,57,62,35,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.179346323013306
1,79,58,17,18,45,118,117,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,68,19,60,64,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.277501106262207
1,73,56,16,18,39,104,104,44,43,44,51,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.028146505355835
1,75,56,15,18,41,112,112,46,45,46,53,45,45,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,174,17,44,67,18,53,56,35,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.955808639526367
1,73,57,15,18,41,106,106,44,43,44,51,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,168,16,42,65,17,51,53,35,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,10.909290790557861
1,73,57,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,171,16,42,63,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.280102014541626
1,75,58,18,18,43,112,112,46,45,46,53,45,45,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,177,17,44,67,19,56,59,37,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,10.99258542060852
1,75,57,15,18,41,108,108,46,45,46,51,45,45,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,171,16,42,65,21,55,60,35,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.316591262817383
1,79,58,19,18,45,120,120,50,49,50,55,49,49,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,187,18,47,71,20,59,63,39,1,1,1,1,1,1,1,1,1,3,2,1,9,81,44,44,6,1,1,11.092773675918579
1,73,57,15,18,41,106,106,44,43,44,51,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,172,16,42,65,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,10.966804027557373
1,71,56,14,18,39,102,102,42,41,42,51,41,41,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,156,16,41,63,19,50,54,33,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.277849435806274
1,79,58,17,18,45,118,118,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,69,19,58,62,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,42,41,6,1,1,11.119897603988647
1,73,56,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,167,16,42,63,17,51,53,35,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.036255598068237
1,77,56,16,18,43,118,118,48,47,48,55,47,47,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,71,19,57,59,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.181584358215332
1,77,58,18,18,43,112,112,48,47,48,53,47,47,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,176,17,44,67,18,56,60,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.176728963851929
1,77,58,16,18,43,114,114,48,47,48,53,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,178,17,44,65,19,58,62,37,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.077479124069214
1,75,56,17,18,41,112,112,46,45,46,53,45,45,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,176,17,44,69,18,53,55,35,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.237483501434326
1,73,56,14,18,39,104,104,44,43,44,51,43,43,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.1346595287323
1,75,58,18,18,43,112,112,46,45,46,53,45,45,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,180,17,45,69,19,57,60,38,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.248454809188843
1,73,57,18,18,43,112,112,46,45,46,53,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,17,45,69,23,60,66,39,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,10.912991523742676
1,77,58,17,18,45,118,118,48,47,48,55,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,186,18,47,71,20,58,61,39,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.0569589138031
1,73,56,16,18,39,103,103,44,43,44,51,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.097052335739136
1,77,58,16,18,43,114,114,48,47,48,53,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,180,17,45,67,19,57,60,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.960843324661255
1,73,57,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,172,16,42,65,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,10.877399682998657
1,73,57,16,18,43,110,110,44,43,44,53,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,181,17,45,69,22,58,63,38,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.189347743988037
1,77,58,17,18,45,118,118,48,47,48,55,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,189,18,48,73,20,59,62,40,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.10829496383667
1,77,58,18,18,47,122,122,48,47,48,57,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,200,19,50,75,26,66,73,41,1,1,1,1,1,1,1,1,1,3,2,1,9,78,43,43,6,1,1,10.972086906433105
1,87,59,34,18,51,168,168,56,55,56,81,55,55,45,9,24,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,352,28,67,114,30,95,98,50,1,1,1,1,1,1,1,1,1,3,2,1,9,112,61,61,6,1,1,11.038999795913696
1,75,56,18,18,43,116,116,46,45,46,55,45,45,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,190,18,47,73,24,61,67,37,1,1,1,1,1,1,1,1,1,3,2,1,9,82,44,44,6,1,1,10.882302045822144
1,79,58,17,18,45,118,118,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,182,18,47,69,19,58,62,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.89523458480835
Binary file added ...er_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.execution_time.png
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ...full-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.qi.png
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
113 changes: 113 additions & 0 deletions evaluation/experiments/program_proofs_example_10_2/full/full.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
// This package contains the full proof for InsertCorrect from
// https://github.com/viperproject/program-proofs-gobra/blob/main/chapter10/examples_10.2.gobra
package full

ghost
requires pq.Valid()
ensures let pqPrime := pq.Insert(y) in
pqPrime.Valid() &&
pqPrime.Elements() == pq.Elements() union mset[int]{y}
decreases len(pq)
pure func (pq PQueue) InsertCorrect(y int) Unit {
return match pq {
case Leaf{}:
Unit{}
case Node{?x, ?l, ?r}:
let pqPrime := pq.Insert(y) in
let min := y < x ? y : x in
let max := y < x ? x : y in
(let newRight := r.Insert(max) in
let _ := asserting(pqPrime == Node{min, newRight, l}) in
let _ := asserting(
let L := len(l.Elements()) in
let R := len(r.Elements()) in
L == R || L == R + 1) in
let _ := r.InsertCorrect(max) in
let _ := asserting(newRight.Valid()) in
let _ := asserting(newRight.IsBalanced()) in
let _ := asserting(l.IsBalanced()) in
let _ := asserting(
let Lprime := len(newRight.Elements()) in
let Rprime := len(l.Elements()) in
Lprime == Rprime || Lprime == Rprime + 1) in
let _ := asserting(pqPrime.IsBalanced()) in
asserting(pqPrime.IsBinaryHeap()))
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Valid() bool {
return pq.IsBinaryHeap() && pq.IsBalanced()
}

ghost
decreases len(pq)
pure func (pq PQueue) Insert(y int) PQueue {
return match pq {
case Leaf{}:
Node{y, Leaf{}, Leaf{}}
case Node{?x, ?left, ?right}:
y < x ? Node{y, right.Insert(x), left} : Node{x, right.Insert(y), left}
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Elements() mset[int] {
return match pq {
case Leaf{}:
mset[int]{}
case Node{?x, ?left, ?right}:
mset[int]{x} union left.Elements() union right.Elements()
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBalanced() (res bool) {
return match pq {
case Leaf{}:
true
case Node{_, ?left, ?right}:
left.IsBalanced() && right.IsBalanced() &&
(let L := len(left.Elements()) in
let R := len(right.Elements()) in
L == R || L == R + 1)
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBinaryHeap() bool {
return match pq {
case Leaf{}:
true
case Node{?x, ?left, ?right}:
left.IsBinaryHeap() && right.IsBinaryHeap() &&
(left == Leaf{} || x <= left.x) &&
(right == Leaf{} || x <= right.x)
}
}


type Unit struct{}

ghost
requires b
decreases
pure func asserting(b bool) Unit {
return Unit{}
}

type PQueue = BraunTree

type BraunTree adt {
Leaf {}

Node {
x int
left BraunTree
right BraunTree
}
}
Loading
Loading