forked from wenhuizhang/summer-school-2020
-
Notifications
You must be signed in to change notification settings - Fork 0
/
exercise02.dfy
38 lines (33 loc) · 932 Bytes
/
exercise02.dfy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
//#title IsPrime II
//#desc Working with an implementation proof
// Here's a correct definition of IsPrime.
// Take another little detour to implementation-land by writing a method
// `test_prime` that implements IsPrime with an imperative while() loop.
predicate divides(factor:nat, candidate:nat)
requires 1<=factor
{
candidate % factor == 0
}
predicate IsPrime(candidate:nat)
{
&& 1<candidate
&& ( forall factor :: 1 < factor < candidate ==> !divides(factor, candidate) )
}
// Convincing the proof to go through requires adding
// a loop invariant and a triggering assert.
method test_prime(candidate:nat) returns (result:bool)
requires 1<candidate
ensures result == IsPrime(candidate)
{
// Fill in the body.
}
method Main()
{
var isprime3 := test_prime(3);
assert isprime3;
var isprime4 := test_prime(4);
assert divides(2, 4);
assert !isprime4;
var isprime5 := test_prime(5);
assert isprime5;
}