From 35aa8c7058c4058c3448885085fcd81ffc897ad3 Mon Sep 17 00:00:00 2001 From: Jonas Date: Fri, 21 Jan 2022 19:02:04 +0100 Subject: [PATCH] Remove superfluous spaces --- docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs | 2 +- docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs | 8 ++++---- docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs | 4 ++-- docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs | 10 +++++----- docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs | 6 +++--- docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs | 10 +++++----- docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs | 10 +++++----- docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs | 6 +++--- docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs | 12 ++++++------ 9 files changed, 34 insertions(+), 34 deletions(-) diff --git a/docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs b/docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs index 14af5689a5b..a1f9d913347 100644 --- a/docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs +++ b/docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs @@ -5,7 +5,7 @@ > List a = Empty | Elem a (List a) - A list is a sum type (Rust: enum) + A list is a sum type (Rust: enum) For now, we only support storing 32-bit integers */ diff --git a/docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs b/docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs index d46f87aadc0..977b53d1424 100644 --- a/docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs +++ b/docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs @@ -16,8 +16,8 @@ help: insert some indirection (e.g., a `Box`, `Rc`, or `&`) to make `List` repre | [Module std::boxed](https://doc.rust-lang.org/std/boxed/index.html): - > Box, casually referred to as a ‘box’, provides the simplest form of heap allocation in Rust. - > Boxes provide ownership for this allocation, and drop their contents when they go out of scope. + > Box, casually referred to as a ‘box’, provides the simplest form of heap allocation in Rust. + > Boxes provide ownership for this allocation, and drop their contents when they go out of scope. */ @@ -32,9 +32,9 @@ pub enum List { Notation: [] = Stack () = Heap A list with three elements looks as follows: - + > [Elem A, ptr] -> (Elem B, ptr) -> (Elem C, ptr) -> (Empty *junk*) - + - The last node is just overhead, the first node is not on the heap - Empty consumes space for a full pointer and an element diff --git a/docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs b/docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs index c50da48add8..f97c1a3a5cb 100644 --- a/docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs +++ b/docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs @@ -7,7 +7,7 @@ // (1) required to enable Prusti's annotations (implemented as Rust macros/attributes) extern crate prusti_contracts; -use prusti_contracts::*; +use prusti_contracts::*; pub struct List { head: Link, @@ -26,7 +26,7 @@ struct Node { impl List { // (3) add a method for length without annotations - // Methods are a special case of function in Rust because of the self argument, + // Methods are a special case of function in Rust because of the self argument, // which doesn't have a declared type. // There are 3 primary forms that self can take: self, &mut self, and &self // We choose &self since computing the length only requires immutable access. diff --git a/docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs b/docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs index 62249419133..02324db5452 100644 --- a/docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs +++ b/docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs @@ -20,7 +20,7 @@ struct Node { /* Chapter 2.4 - Push - So let's write pushing a value onto a list. + So let's write pushing a value onto a list. push mutates the list, so we'll want to take &mut self */ @@ -41,7 +41,7 @@ impl List { /* // (2) compile this before proceeding pub fn push(&mut self, elem: i32) { - + let new_node = Node { elem: elem, next: self.head, // this should be the old list @@ -53,7 +53,7 @@ impl List { } */ - /* + /* // (3) What if we put something back? Namely, the node that we're creating. // Rust does not accept this for exception safety. pub fn push(&mut self, elem: i32) { @@ -61,7 +61,7 @@ impl List { elem: elem, next: self.head, }); - + self.head = Link::More(new_node); } */ @@ -74,7 +74,7 @@ impl List { elem: elem, next: mem::replace(&mut self.head, Link::Empty), }); - + self.head = Link::More(new_node); } diff --git a/docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs b/docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs index 80955b51a07..2381577372f 100644 --- a/docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs +++ b/docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs @@ -51,12 +51,12 @@ impl List { // a) The length of the list increases by one: check // b) The first element is the pushed one // c) All other elements have not been changed - #[ensures(self.len() == old(self.len()) + 1)] + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] // (2) express property b) pub fn push(&mut self, elem: i32) { let new_node = Box::new(Node { elem: elem, - next: replace(&mut self.head, Link::Empty), + next: replace(&mut self.head, Link::Empty), }); self.head = Link::More(new_node); @@ -85,7 +85,7 @@ impl Link { // (4) #[pure] - #[requires(0 <= index && index < self.len())] // (6) no fix as there's no + #[requires(0 <= index && index < self.len())] // (6) no fix as there's no // relation between being empty and length 0 pub fn lookup(&self, index: usize) -> i32 { match self { diff --git a/docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs b/docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs index 42144399bce..b093f038c79 100644 --- a/docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs +++ b/docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs @@ -22,8 +22,8 @@ struct Node { #[ensures(dest.is_empty())] #[ensures(old(dest.len()) == result.len())] // (5) make sure that replace leaves elements in the result untouched -//#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> -// old(dest.lookup(i)) == result.lookup(i)))] +//#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> +// old(dest.lookup(i)) == result.lookup(i)))] fn replace(dest: &mut Link, src: Link) -> Link { mem::replace(dest, src) } @@ -53,10 +53,10 @@ impl List { // a) The length of the list increases by one: check // b) The first element is the pushed one: check // c) All other elements have not been changed - #[ensures(self.len() == old(self.len()) + 1)] + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==> - old(self.lookup(i-1)) == self.lookup(i)))] // (2) specify property c) + old(self.lookup(i-1)) == self.lookup(i)))] // (2) specify property c) // Why does it fail? // The spec for replace is not strong enough! pub fn push(&mut self, elem: i32) { @@ -90,7 +90,7 @@ impl Link { } #[pure] - #[requires(0 <= index && index < self.len())] + #[requires(0 <= index && index < self.len())] pub fn lookup(&self, index: usize) -> i32 { match self { Link::Empty => unreachable!(), diff --git a/docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs b/docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs index c0ca264f3ef..f70bbd7f866 100644 --- a/docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs +++ b/docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs @@ -1,8 +1,8 @@ /* Chapter 2.5 Pop - Like push, pop wants to mutate the list. - Unlike push, we actually want to return something. + Like push, pop wants to mutate the list. + Unlike push, we actually want to return something. But pop also has to deal with a tricky corner case: what if the list is empty? To represent this case, we introduce an Option type. (Option is actually in the standard library but we write our own to assign specs to functions) @@ -37,8 +37,8 @@ struct Node { #[requires(src.is_empty())] #[ensures(dest.is_empty())] #[ensures(old(dest.len()) == result.len())] -#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> - old(dest.lookup(i)) == result.lookup(i)))] +#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> + old(dest.lookup(i)) == result.lookup(i)))] fn replace(dest: &mut Link, src: Link) -> Link { mem::replace(dest, src) } @@ -64,7 +64,7 @@ impl List { } } - #[ensures(self.len() == old(self.len()) + 1)] + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))] diff --git a/docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs b/docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs index b3cd07fb980..475bb8fde1d 100644 --- a/docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs +++ b/docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs @@ -54,8 +54,8 @@ struct Node { #[requires(src.is_empty())] #[ensures(dest.is_empty())] #[ensures(old(dest.len()) == result.len())] -#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> - old(dest.lookup(i)) == result.lookup(i)))] +#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> + old(dest.lookup(i)) == result.lookup(i)))] fn replace(dest: &mut Link, src: Link) -> Link { mem::replace(dest, src) } @@ -81,7 +81,7 @@ impl List { } } - #[ensures(self.len() == old(self.len()) + 1)] + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))] diff --git a/docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs b/docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs index 46fbadf1b58..8853dd50db2 100644 --- a/docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs +++ b/docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs @@ -1,8 +1,8 @@ /* Chapter 2.6 - Testing - Alright, so we've got push and pop written, now we can actually test out our stack! - Rust and cargo support testing as a first-class feature, - so this will be super easy. + Alright, so we've got push and pop written, now we can actually test out our stack! + Rust and cargo support testing as a first-class feature, + so this will be super easy. All we have to do is write a function, and annotate it with #[test]. */ @@ -60,8 +60,8 @@ struct Node { #[requires(src.is_empty())] #[ensures(dest.is_empty())] #[ensures(old(dest.len()) == result.len())] -#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> - old(dest.lookup(i)) == result.lookup(i)))] +#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> + old(dest.lookup(i)) == result.lookup(i)))] fn replace(dest: &mut Link, src: Link) -> Link { mem::replace(dest, src) } @@ -87,7 +87,7 @@ impl List { } } - #[ensures(self.len() == old(self.len()) + 1)] + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))]