Skip to content

Commit e04e90c

Browse files
bsdinisbsdinis
committed
resource: rename example dir
1 parent 1c96d32 commit e04e90c

6 files changed

Lines changed: 41 additions & 41 deletions

File tree

examples/pcm/agreement.rs renamed to examples/resource/agreement.rs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -134,12 +134,12 @@ impl<T> AgreementResource<T> {
134134
requires
135135
old(self).inv(),
136136
ensures
137-
final(self).inv(),
137+
self.inv(),
138138
result.inv(),
139-
final(self).id() == old(self).id(),
139+
self.id() == old(self).id(),
140140
result.id() == old(self).id(),
141-
final(self)@ == result@,
142-
final(self)@ == old(self)@,
141+
self@ == result@,
142+
self@ == old(self)@,
143143
{
144144
let tracked r = resource::duplicate(&self.r);
145145
AgreementResource::<T> { r }
@@ -154,9 +154,9 @@ impl<T> AgreementResource<T> {
154154
other.inv(),
155155
old(self).id() == other.id(),
156156
ensures
157-
final(self).id() == old(self).id(),
158-
final(self)@ == old(self)@,
159-
final(self)@ == other@,
157+
self.id() == old(self).id(),
158+
self@ == old(self)@,
159+
self@ == other@,
160160
{
161161
self.r.validate_2(&other.r);
162162
}

examples/pcm/count_to_two.rs renamed to examples/resource/count_to_two.rs

File renamed without changes.

examples/pcm/log.rs renamed to examples/resource/log.rs

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -222,9 +222,9 @@ impl<T> LogResource<T> {
222222
requires
223223
old(self)@ is FullAuthority,
224224
ensures
225-
final(self)@ is FullAuthority,
226-
final(self).id() == old(self).id(),
227-
final(self)@.log() == old(self)@.log() + seq![v],
225+
self@ is FullAuthority,
226+
self.id() == old(self).id(),
227+
self@.log() == old(self)@.log() + seq![v],
228228
{
229229
let value = LogResourceValue::<T>::FullAuthority { log: self@.log() + seq![v] };
230230
update_mut(&mut self.r, value);
@@ -236,11 +236,11 @@ impl<T> LogResource<T> {
236236
old(other)@ is HalfAuthority,
237237
old(self).id() == old(other).id(),
238238
ensures
239-
final(self)@ is HalfAuthority,
240-
final(self).id() == old(self).id(),
241-
final(other).id() == old(self).id(),
242-
final(self)@.log() == old(self)@.log() + seq![v],
243-
final(other)@ == final(self)@,
239+
self@ is HalfAuthority,
240+
self.id() == old(self).id(),
241+
other.id() == old(self).id(),
242+
self@.log() == old(self)@.log() + seq![v],
243+
other@ == self@,
244244
{
245245
self.r.validate_2(&other.r);
246246
let new_log = self@.log() + seq![v];
@@ -263,12 +263,12 @@ impl<T> LogResource<T> {
263263
requires
264264
old(self).id() == other.id(),
265265
ensures
266-
final(self)@ == old(self)@,
267-
is_prefix(final(self)@.log(), other@.log()) || is_prefix(other@.log(), final(self)@.log()),
268-
final(self)@ is HalfAuthority ==> is_prefix(other@.log(), final(self)@.log()),
269-
final(self)@ is FullAuthority ==> is_prefix(other@.log(), final(self)@.log()),
270-
other@ is HalfAuthority ==> is_prefix(final(self)@.log(), other@.log()),
271-
other@ is FullAuthority ==> is_prefix(final(self)@.log(), other@.log()),
266+
self@ == old(self)@,
267+
is_prefix(self@.log(), other@.log()) || is_prefix(other@.log(), self@.log()),
268+
self@ is HalfAuthority ==> is_prefix(other@.log(), self@.log()),
269+
self@ is FullAuthority ==> is_prefix(other@.log(), self@.log()),
270+
other@ is HalfAuthority ==> is_prefix(self@.log(), other@.log()),
271+
other@ is FullAuthority ==> is_prefix(self@.log(), other@.log()),
272272
{
273273
self.r.validate_2(&other.r)
274274
}

examples/pcm/monotonic_counter.rs renamed to examples/resource/monotonic_counter.rs

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -260,8 +260,8 @@ impl MonotonicCounterResource {
260260
requires
261261
old(self)@ is FullRightToAdvance,
262262
ensures
263-
final(self).id() == old(self).id(),
264-
final(self)@ == (MonotonicCounterResourceValue::FullRightToAdvance {
263+
self.id() == old(self).id(),
264+
self@ == (MonotonicCounterResourceValue::FullRightToAdvance {
265265
value: old(self)@->FullRightToAdvance_value + 1,
266266
}),
267267
{
@@ -284,10 +284,10 @@ impl MonotonicCounterResource {
284284
old(other)@ is HalfRightToAdvance,
285285
ensures
286286
old(self)@ == old(other)@,
287-
final(self).id() == old(self).id(),
288-
final(other).id() == old(self).id(),
289-
final(other)@ == final(self)@,
290-
final(self)@ == (MonotonicCounterResourceValue::HalfRightToAdvance {
287+
self.id() == old(self).id(),
288+
other.id() == old(self).id(),
289+
other@ == self@,
290+
self@ == (MonotonicCounterResourceValue::HalfRightToAdvance {
291291
value: old(self)@->HalfRightToAdvance_value + 1,
292292
}),
293293
{
@@ -313,11 +313,11 @@ impl MonotonicCounterResource {
313313
requires
314314
old(self).id() == other.id(),
315315
ensures
316-
final(self)@ == old(self)@,
317-
final(self)@ is LowerBound && other@ is FullRightToAdvance ==> final(self)@.n() <= other@.n(),
318-
other@ is LowerBound && final(self)@ is FullRightToAdvance ==> other@.n() <= final(self)@.n(),
319-
final(self)@ is LowerBound && other@ is HalfRightToAdvance ==> final(self)@.n() <= other@.n(),
320-
other@ is LowerBound && final(self)@ is HalfRightToAdvance ==> other@.n() <= final(self)@.n(),
316+
self@ == old(self)@,
317+
self@ is LowerBound && other@ is FullRightToAdvance ==> self@.n() <= other@.n(),
318+
other@ is LowerBound && self@ is FullRightToAdvance ==> other@.n() <= self@.n(),
319+
self@ is LowerBound && other@ is HalfRightToAdvance ==> self@.n() <= other@.n(),
320+
other@ is LowerBound && self@ is HalfRightToAdvance ==> other@.n() <= self@.n(),
321321
{
322322
self.r.validate_2(&other.r)
323323
}

examples/pcm/oneshot.rs renamed to examples/resource/oneshot.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ impl OneShotResource {
194194
requires
195195
old(self)@ is FullRightToComplete,
196196
ensures
197-
final(self)@ is Complete,
197+
self@ is Complete,
198198
{
199199
let v = OneShotResourceValue::Complete { };
200200
update_mut(&mut self.r, v);
@@ -221,10 +221,10 @@ impl OneShotResource {
221221
!(old(other)@ is Empty),
222222
ensures
223223
old(other)@ is HalfRightToComplete,
224-
final(self)@ is Complete,
225-
final(other)@ is Complete,
226-
final(self).id() == old(self).id(),
227-
final(other).id() == old(self).id(),
224+
self@ is Complete,
225+
other@ is Complete,
226+
self.id() == old(self).id(),
227+
other.id() == old(self).id(),
228228
{
229229
self.r.validate();
230230
other.r.validate();
@@ -258,9 +258,9 @@ impl OneShotResource {
258258
other@ is Complete,
259259
!(old(self)@ is Empty),
260260
ensures
261-
final(self).id() == old(self).id(),
262-
final(self)@ == old(self)@,
263-
final(self)@ is Complete,
261+
self.id() == old(self).id(),
262+
self@ == old(self)@,
263+
self@ is Complete,
264264
{
265265
self.r.validate_2(&other.r);
266266
}

‎source/rust_verify_test/tests/examples.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ enum Mode {
1616

1717
examples_in_dir!("../../examples");
1818
examples_in_dir!("../../examples/guide");
19-
examples_in_dir!("../../examples/pcm");
19+
examples_in_dir!("../../examples/resource");
2020
examples_in_dir!("../../examples/state_machines");
2121
examples_in_dir!("../../examples/summer_school");
2222
examples_in_dir!("../../examples/state_machines/tutorial");

0 commit comments

Comments
 (0)