-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
114 changed files
with
3,531 additions
and
0 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
[package] | ||
name = "chapter1" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
prusti-contracts = { path = "/r/prusti-dev-master/prusti-contracts/prusti-contracts" } | ||
# prusti-contracts = "0.1.9" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
check_overflows = false | ||
|
||
# FUTURE: numberOfErrorsToReport | ||
# See: https://github.com/viperproject/prusti-dev/issues/1213 | ||
extra_verifier_args = ["--numberOfErrorsToReport=0"] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
// All of these examples work as expected: | ||
pub mod example_1_0; | ||
pub mod example_1_1; | ||
// pub mod example_1_2; // Should and does fail | ||
pub mod example_1_3_1; | ||
pub mod example_1_3_2; | ||
// pub mod example_1_4_1; // Should and does fail | ||
pub mod example_1_5_0; | ||
pub mod example_1_6_1; | ||
pub mod example_1_6_2; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
// 1.0.dfy | ||
// method Triple (x: int) returns (r:int) | ||
|
||
pub fn triple(x: i64) -> i64 { | ||
let y = 2 * x; | ||
x + y | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
// 1.1.dfy | ||
// method Triple(x: int) returns (r: int) | ||
|
||
pub fn triple(x: i64) -> i64 { | ||
let y = 2 * x; | ||
let r = x + y; | ||
assert!(r == 3 * x); | ||
r | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
// 1.2.dfy | ||
// method Triple(x: int) returns (r: int) | ||
|
||
// Disable clippy warning for assert!(false); | ||
#[allow(clippy::assertions_on_constants)] | ||
|
||
// Note: This file correctly fails verification | ||
|
||
// FUTURE: numberOfErrorsToReport | ||
// Here Prusti should show that (r < 5) is correct, since (r == 10 * x) was checked a line before. | ||
// See: https://github.com/viperproject/prusti-dev/issues/1213 | ||
pub fn triple(x: i64) -> i64 { | ||
let y = 2 * x; | ||
let r = x + y; | ||
assert!(r == 10 * x); // Prusti finds error here | ||
assert!(r < 5); // not checked, but should be correct | ||
assert!(false); // not checked, but should be shown as incorrect | ||
r | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
// 1.3_1.dfy | ||
// method Triple(x: int) returns (r: int) | ||
|
||
pub fn triple(x: i64) -> i64 { | ||
let r = if x == 0 { | ||
0 | ||
} else { | ||
let y = 2 * x; | ||
x + y | ||
}; | ||
assert!(r == 3 * x); | ||
r | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
// 1.3_2.dfy | ||
// method Triple(x: int) returns (r: int) | ||
|
||
pub fn triple(x: i64) -> i64 { | ||
// Note: this translation is not a direct mapping because Dafny uses | ||
// a non-deterministic choice here. | ||
let r = if x < 18 { | ||
let a = 2 * x; | ||
let b = 4 * x; | ||
(a + b) / 2 | ||
} else if 0 <= x { | ||
let y = 2 * x; | ||
x + y | ||
} else { | ||
unreachable!(); | ||
}; | ||
assert!(r == 3 * x); | ||
r | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
// 1.4_1.dfy | ||
// method Triple(x: int) returns (r: int) | ||
// method Caller() | ||
|
||
// Note: This file correctly fails verification | ||
|
||
pub fn triple(x: i64) -> i64 { | ||
// Note: this translation is not a direct mapping because Dafny uses | ||
// a non-deterministic choice here. | ||
let r = match x { | ||
x if x < 18 => { | ||
let a = 2 * x; | ||
let b = 4 * x; | ||
(a + b) / 2 | ||
} | ||
x if 0 <= x => { | ||
let y = 2 * x; | ||
x + y | ||
} | ||
_ => { | ||
unreachable!(); | ||
} | ||
}; | ||
assert!(r == 3 * x); | ||
r | ||
} | ||
|
||
pub fn caller() { | ||
let t = triple(18); | ||
assert!(t < 100); // cannot be proven due to missing postcondition of triple | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.5.0.dfy | ||
// method Triple(x: int) returns (r: int) | ||
// ghost method DoubleQuadruple(x: int) returns (a: int, b: int) | ||
|
||
#[ensures(result == x * 3)] | ||
pub fn triple(x: i64) -> i64 { | ||
let y = 2 * x; | ||
let r = x + y; | ||
|
||
//FUTURE: ghost_variables | ||
let (a, b) = ghost_double_quadruple(x); | ||
prusti_assert!((a <= r && r <= b) || (b <= r && r <= a)); | ||
r | ||
} | ||
|
||
// FUTURE: ghost_functions | ||
#[pure] | ||
fn ghost_double_quadruple(x: i64) -> (i64, i64) { | ||
(2 * x, 4 * x) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.6_1.dfy | ||
// function Average(a: int, b: int): int | ||
// method Triple'(x: int) returns (r: int) | ||
|
||
#[pure] | ||
pub fn average(a: i64, b: i64) -> i64 { | ||
(a + b) / 2 | ||
} | ||
|
||
#[ensures(average(result, x * 3) == x * 3)] | ||
pub fn triple_wrong(x: i64) -> i64 { | ||
x * 3 + 1 | ||
} | ||
|
||
#[ensures(average(result, x * 3) == x * 3)] | ||
#[ensures(result % 2 == (x * 3) % 2)] | ||
pub fn triple_correct(x: i64) -> i64 { | ||
x * 3 | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.6_2.dfy | ||
// predicate IsEven(x: int) | ||
// function IsEven2(x: int): bool | ||
|
||
#[pure] | ||
#[ensures(result == (x % 2 == 0))] // technically not needed due to #[pure] | ||
pub fn is_even(x: i64) -> bool { | ||
x % 2 == 0 | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
// All these exercises can be verified as expected | ||
pub mod exercise_1_0; | ||
pub mod exercise_1_1; | ||
pub mod exercise_1_2; | ||
pub mod exercise_1_3; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.0.dfy | ||
// method Min(x: int, y: int) returns (m: int) | ||
|
||
#[ensures(result <= x && result <= y)] | ||
pub fn min(x: i64, y: i64) -> i64 { | ||
if x < y { | ||
x - 1 | ||
} else { | ||
y - 1 | ||
} | ||
// FUTURE: std_lib_extern_spec_enhancement | ||
// x.min(y) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.1.dfy | ||
// method MaxSum(x: int, y: int) returns (s: int, m: int) | ||
// method CallMaxSum() returns (s: int, m: int) | ||
|
||
#[ensures(result.0 == x + y)] | ||
#[ensures(result.1 >= x && result.1 >= y)] | ||
#[ensures(result.1 == x || result.1 == y)] | ||
pub fn max_sum(x: i64, y: i64) -> (i64, i64) { | ||
let s = x + y; | ||
let m = if x > y { x } else { y }; | ||
(s, m) | ||
// FUTURE: std_lib_extern_spec_enhancement | ||
// (x + y, x.max(y)) | ||
} | ||
|
||
pub fn call_max_sum() -> (i64, i64) { | ||
let (s, m) = max_sum(1928, 1); | ||
prusti_assert!(s == 1929); | ||
prusti_assert!(m == 1928); | ||
(s, m) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.2.dfy | ||
// method MaxSum(x: int, y: int) returns (s: int, m: int) | ||
// method ReconstructFromMaxSum(s: int, m: int) returns (x: int, y: int) | ||
// method TestMaxSum(x: int, y: int) | ||
|
||
use super::exercise_1_1::max_sum; | ||
|
||
#[ensures(s == result.0 + result.1)] | ||
#[ensures((m == result.0 || m == result.1) && result.0 <= m && result.1 <= m)] | ||
#[requires(s <= 2 * m)] | ||
pub fn reconstruct_from_max_sum(s: i64, m: i64) -> (i64, i64) { | ||
let x = m; | ||
let y = s - m; | ||
(x, y) | ||
} | ||
|
||
pub fn test_max_sum(x: i64, y: i64) { | ||
let (s, m) = max_sum(x, y); | ||
let (x_, y_) = reconstruct_from_max_sum(s, m); | ||
prusti_assert!((x_ == x && y_ == y) || (x_ == y && y_ == x)); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
use prusti_contracts::*; | ||
|
||
// 1.3.dfy | ||
// function Average(a: int, b: int): int | ||
// method Triple'(x: int) returns (r: int) | ||
|
||
#[pure] | ||
pub fn average(a: i64, b: i64) -> i64 { | ||
(a + b) / 2 | ||
} | ||
|
||
#[ensures(average(result, x * 3) == x * 3)] | ||
pub fn triple_(x: i64) -> i64 { | ||
x * 3 + 1 | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
// #![warn(clippy::pedantic)] | ||
|
||
#[allow(clippy::wildcard_imports)] | ||
#[allow(unused)] | ||
mod examples; | ||
|
||
#[allow(clippy::wildcard_imports)] | ||
#[allow(unused)] | ||
mod exercises; |
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
[package] | ||
name = "chapter2" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
prusti-contracts = "0.1.4" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
check_overflows = false |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
pub mod example_2_0; | ||
pub mod example_2_3_0; | ||
pub mod example_2_3_1; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
use prusti_contracts::*; | ||
|
||
// 2.0.dfy | ||
// method MyMethod(x: int) returns (y: int) | ||
|
||
#[requires(10 <= x)] | ||
#[ensures(25 <= result)] | ||
pub fn my_method(x: i64) -> i64 { | ||
let a = x + 3; | ||
let b = 12; | ||
a + b | ||
} | ||
|
||
#[allow(clippy::let_and_return)] | ||
#[requires(10 <= x)] | ||
#[ensures(25 <= result)] | ||
pub fn my_method_with_backwards_annotations(x: i64) -> i64 { | ||
prusti_assert!(10 <= x); | ||
prusti_assert!(25 <= x + 3 + 12); | ||
let a = x + 3; | ||
prusti_assert!(25 <= a + 12); | ||
let b = 12; | ||
prusti_assert!(25 <= a + b); | ||
let result = a + b; | ||
prusti_assert!(25 <= result); // postcondition | ||
result | ||
} | ||
|
||
#[allow(clippy::let_and_return)] | ||
#[requires(10 <= x)] | ||
#[ensures(25 <= result)] | ||
pub fn my_method_with_forwards_annotations(x: i64) -> i64 { | ||
prusti_assert!(10 <= x); // precondition | ||
let a = x + 3; | ||
prusti_assert!(10 <= x && a == x + 3); | ||
let b = 12; | ||
prusti_assert!(10 <= x && a == x + 3 && b == 12); | ||
let result = a + b; | ||
prusti_assert!(10 <= x && a == x + 3 && b == 12 && result == a + b); | ||
prusti_assert!(25 <= result); | ||
result | ||
} |
Oops, something went wrong.