clarify changed init signature

[web.git] / ralf / _posts / 2018-04-05-a-formal-look-at-pinning.md

diff --git a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
index 4aed608945629e1ac8b10b4659ee213fc7aabfe8..98b53a18eea36c911f55de6f30f4733c83da360b 100644 (file)
--- a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -89,7 +89,7 @@ fn main() {
 The most intersting piece of code here is `read_ref`, which dereferences a raw pointer.
 The reason this is legal is that we can rely on the entire `SelfReferential` not having been moved since `init()` was called (which is the only place that would set the pointer to `Some`).
 
-In particular, if we changed the signature of `init()` to take `&mut`, we could easily cause UB by writing the following code:
+In particular, if we changed the signature to `fn init(&mut self)`, we could easily cause UB by writing the following code:
 {% highlight rust %}
 fn main() {
     // Create an initialize a SelfReferential in a Box, move it out, and drop the Box
@@ -154,6 +154,8 @@ Formally:
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
   ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```
 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
   borrowed('a,
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
@@ -166,6 +168,8 @@ This could look as follows:
 ```
 Box<T>.own(ptr: Pointer) :=
   exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```
 (&'a mut T).own(ptr: Pointer) :=
   borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```
@@ -223,6 +227,8 @@ A list of bytes makes a valid `PinBox<T>` if those bytes form a pointer `ptr` su
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)
+```
+```
 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```