Remove superfluous spaces

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
 */

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<T>, 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<T>, 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
 

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.

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,15 +53,15 @@ 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) {
         let new_node = Box::new(Node {
             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);
     }
 

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 {

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!(),

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)))]

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)))]

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)))]