Add proof outline syntax support

README.md

@@ -36,60 +36,39 @@ small-step semantics and verifies the given derivations.
 
 ### IMP Syntax
 The core IMP syntax is precisely the same as introduced in the lecture (incl. shorthands). 
-The syntax for pre-/post-conditions is a bit cumbersome, however; every 'base' statement must
-have a pre- and post-condition, rules of consequence are implicit at sequence statements.
+The syntax to verify axiomatic derivations is the same as the introduced "Proof Outline", except that there
+are no semi-colons.
 
 Example (`square.imp`, squares `a` and stores it in `b` using only addition):
 ```
-# an "ergonomic" proof outline as in the course:
+# proof outline as in the course:
 {a >= 0}
 ⊨
-{a >= 0 and 0 = 0 and 0 = 0} 
-b := 0;
+{a >= 0 and 0 = 0 and 0 = 0}
+b := 0
 {a >= 0 and b = 0 and 0 = 0}
-i := 0;
+i := 0
 {a >= 0 and b = 0 and i = 0}
 ⊨
 {i <= a and b = a * i}
 while (i # a) do
     {i # a and (i <= a and b = a * i)}
     ⊨
     {i # a and (i <= a and b + a = a * (i + 1))}
-    b := b + a;
+    b := b + a
     {i # a and (i <= a and b = a * (i + 1))}
     ⊨
     {i + 1 <= a and b = a * (i + 1)}
-    i := i + 1;
+    i := i + 1
     {i <= a and b = a * i}
 end
 {not (i # a) and (i <= a and b = a * i)}
 ⊨
 {b = a * a}
-
-
-# the equivalent cumbersome notation of this project (currently):
-{a >= 0} skip {a >= 0};
-{a >= 0 and 0 = 0} b := 0 {a >= 0 and b = 0};
-{a >= 0 and b = 0 and 0 = 0} i := 0 {a >= 0 and b = 0 and i = 0};
-{i <= a and b = a * i}
-while (i # a) do
-    {i # a and (i <= a and b = a * i)}
-    skip
-    {i # a and (i <= a and b = a * i)};
-    {i # a and (i <= a and b + a = a * (i + 1))}
-    b := b + a
-    {i # a and (i <= a and b = a * (i + 1))};
-    {i + 1 <= a and b = a * (i + 1)}
-    i := i + 1
-    {i <= a and b = a * i}
-end
-{not (i # a) and (i <= a and b = a * i)};
-{b = a * a}
-skip
-{b = a * a}
 ```
 
-Note in particular the use of `;` and `skip` to imitate `⊨`. Additionally, one must be very careful
+Note that you may use `⊨` or `|=` for rules of consequence.  
+Additionally, one must be very careful
 writing the conditions for `if` and `while` - their conditions must be ANDed at the highest level: 
 ```
 # this is okay (note the parentheses that force precedence)

examples/square.imp

@@ -1,19 +1,23 @@
-{a >= 0} skip {a >= 0};
-{a >= 0 and 0 = 0} b := 0 {a >= 0 and b = 0};
-{a >= 0 and b = 0 and 0 = 0} i := 0 {a >= 0 and b = 0 and i = 0};
+{a >= 0}
+⊨
+{a >= 0 and 0 = 0 and 0 = 0}
+b := 0
+{a >= 0 and b = 0 and 0 = 0}
+i := 0
+{a >= 0 and b = 0 and i = 0}
+⊨
 {i <= a and b = a * i}
 while (i # a) do
     {i # a and (i <= a and b = a * i)}
-    skip
-    {i # a and (i <= a and b = a * i)};
+    ⊨
     {i # a and (i <= a and b + a = a * (i + 1))}
     b := b + a
-    {i # a and (i <= a and b = a * (i + 1))};
+    {i # a and (i <= a and b = a * (i + 1))}
+    ⊨
     {i + 1 <= a and b = a * (i + 1)}
     i := i + 1
     {i <= a and b = a * i}
 end
-{not (i # a) and (i <= a and b = a * i)};
-{b = a * a}
-skip
+{not (i # a) and (i <= a and b = a * i)}
+⊨
 {b = a * a}

examples/swap.imp

@@ -1,3 +1,9 @@
-{x = X and y = Y} z := x {z = X and y = Y};
-{y = Y and z = X} x := y {x = Y and z = X};
-{x = Y and z = X} y := z {x = Y and y = X}
+{x = X and y = Y}
+z := x
+{z = X and y = Y}
+|=
+{y = Y and z = X}
+x := y
+{x = Y and z = X}
+y := z
+{x = Y and y = X}

src/ast.rs

@@ -4,6 +4,112 @@ use z3::ast::Ast;
 
 pub type Var = String;
 
+#[derive(Clone, Debug)]
+pub struct AssertionChain(pub Vec<Bexp>);
+
+impl AssertionChain {
+    pub fn new(first: Box<Bexp>, rem: Vec<Box<Bexp>>) -> AssertionChain {
+        let mut rem: Vec<Bexp> = rem.into_iter().map(|bexp_box| *bexp_box ).collect();
+        rem.insert(0, *first);
+        AssertionChain(rem)
+    }
+
+    pub fn indent_string(&self, prefix: String) -> String {
+        let mut result = format!("{}{{ {:?} }}", prefix.clone(), self.0.first().unwrap());
+
+        for assertion in self.0.iter().skip(1) {
+            result += &format!("\n{}⊨\n{}{{ {:?} }}", prefix.clone(), prefix.clone(), assertion)
+        }
+
+        result
+    }
+}
+
+#[derive(Clone)]
+pub struct AxBlock(pub AssertionChain, pub Vec<(AxStm, AssertionChain)>);
+
+impl AxBlock {
+    pub fn indent_string(&self, prefix: String) -> String {
+        let first = &self.0;
+        let rem = &self.1;
+
+        let mut res = format!("{}", first.indent_string(prefix.clone()));
+
+        for (stm, chain) in rem.iter() {
+            res += &format!("\n{}", stm.indent_string(prefix.clone()));
+            res += &format!("\n{}", chain.indent_string(prefix.clone()));
+        }
+
+        res
+
+    }
+
+    pub fn into_stm(self) -> Box<Stm> {
+        let AxBlock(_, rem) = self;
+        let mut rem = rem.into_iter();
+        let mut pre_stm = rem.next().unwrap().0.into_stm();
+
+        for (curr_stm, _) in rem {
+            pre_stm = Box::new(Stm::Seq(pre_stm, curr_stm.into_stm()))
+        }
+
+        pre_stm
+    }
+}
+
+impl Debug for AxBlock {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        f.write_str(&self.indent_string("".to_owned()))
+    }
+}
+
+
+#[derive(Clone, Debug)]
+pub enum AxStm {
+    Assign(Var, Aexp),
+    Skip,
+    If(Bexp, AxBlock, AxBlock),
+    While(Bexp, AxBlock),
+}
+
+impl AxStm {
+    pub fn into_stm(self) -> Box<Stm> {
+        Box::new(match self {
+            AxStm::Skip => Stm::Skip,
+            AxStm::Assign(v, e) => Stm::Assign(v, Box::new(e)),
+            AxStm::If(cond, then_block, else_block) => {
+                let then_stm = then_block.into_stm();
+                let else_stm = else_block.into_stm();
+                Stm::If(Box::new(cond), then_stm, else_stm)
+            },
+            AxStm::While(cond, inner_block) => {
+                let inner_stm = inner_block.into_stm();
+                Stm::While(Box::new(cond), inner_stm)
+            }
+        })
+    }
+
+    pub fn indent_string(&self, prefix: String) -> String {
+        match self {
+            AxStm::Skip => prefix + "skip",
+            AxStm::Assign(v, aexp) => prefix + &format!("{} := {:?}", v, aexp),
+            AxStm::If(cond, then_block, else_block) => {
+                let then_string = then_block.indent_string(prefix.clone() + "    ");
+                let else_string = else_block.indent_string(prefix.clone() + "    ");
+
+                format!("{}if {:?} then\n{}\nelse{}\nend", prefix, cond, then_string, else_string)
+            },
+            AxStm::While(cond, inner_block) => {
+                let inner_string = inner_block.indent_string(prefix.clone() + "    ");
+
+                format!("{}while {:?} do\n{}\nend", prefix, cond, inner_string)
+            },
+        }
+    }
+}
+
+
+
 #[derive(Clone)]
 pub enum StmAx {
     Assign(Box<Bexp>, Var, Box<Aexp>, Box<Bexp>),