File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -32,6 +32,8 @@ fn test_job_start_success() {
3232#[ test]
3333#[ should_panic( expected = "Precondition failed: matches! (self.state, State::Idle)" ) ]
3434fn test_job_start_panics_if_not_idle ( ) {
35- let mut job = Job { state : State :: Running } ;
35+ let mut job = Job {
36+ state : State :: Running ,
37+ } ;
3638 job. start ( ) ; // This violates the precondition.
3739}
Original file line number Diff line number Diff line change @@ -16,14 +16,20 @@ impl Counter {
1616
1717#[ test]
1818fn test_increment_success ( ) {
19- let mut c = Counter { count : 5 , capacity : 10 } ;
19+ let mut c = Counter {
20+ count : 5 ,
21+ capacity : 10 ,
22+ } ;
2023 c. increment ( ) ;
2124 assert_eq ! ( c. count, 6 ) ;
2225}
2326
2427#[ test]
2528#[ should_panic( expected = "Postcondition failed: self.count <= self.capacity" ) ]
2629fn test_increment_violates_invariant ( ) {
27- let mut c = Counter { count : 10 , capacity : 10 } ;
30+ let mut c = Counter {
31+ count : 10 ,
32+ capacity : 10 ,
33+ } ;
2834 c. increment ( ) ; // This will make count 11, violating the invariant on exit.
2935}
Original file line number Diff line number Diff line change @@ -6,7 +6,11 @@ use anodized::contract;
66 ensures: |val| val % 2 == 0 ,
77) ]
88fn calculate_even_result ( output : i32 ) -> i32 {
9- if output % 2 == 0 { output + 2 } else { output + 1 }
9+ if output % 2 == 0 {
10+ output + 2
11+ } else {
12+ output + 1
13+ }
1014}
1115
1216#[ test]
@@ -20,7 +24,11 @@ fn test_rename_success() {
2024fn test_rename_panics_if_not_even ( ) {
2125 #[ contract( returns: result, ensures: |val| val % 2 == 0 ) ]
2226 fn calculate_odd_result ( output : i32 ) -> i32 {
23- if output % 2 == 0 { output + 1 } else { output + 2 }
27+ if output % 2 == 0 {
28+ output + 1
29+ } else {
30+ output + 2
31+ }
2432 }
2533 calculate_odd_result ( 4 ) ; // Returns 5, violating the postcondition.
2634}
You can’t perform that action at this time.
0 commit comments