Merge branch 'develop' into adinapoli/polish-docs

Author: ranjitjhala

Diff for: benchmarks/cse230/LICENSE

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2014 Dr. Kat
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

Diff for: benchmarks/cse230/README.md

@@ -0,0 +1 @@
+Retrieved from: https://github.com/ucsd-progsys/230-wi19-web/

Diff for: benchmarks/cse230/src/Week10/Axiomatic.hs

@@ -0,0 +1,364 @@
+{-@ LIQUID "--reflection"  @-}
+{-@ LIQUID "--ple"         @-}
+{-@ LIQUID "--diff"        @-}
+{- LIQUID "--short-names" @-}
+{-@ infixr ++              @-}  -- TODO: Silly to have to rewrite this annotation!
+{-@ infixr <~              @-}  -- TODO: Silly to have to rewrite this annotation!
+
+--------------------------------------------------------------------------------
+-- | Inspired by 
+--     http://flint.cs.yale.edu/cs428/coq/sf/Hoare.html
+--     http://flint.cs.yale.edu/cs428/coq/sf/Hoare2.html
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs #-}
+
+module Axiomatic where
+
+import           Prelude hiding ((++)) 
+import           ProofCombinators
+import qualified State as S
+import           Expressions  
+import           Imp 
+import           BigStep hiding (And)
+
+--------------------------------------------------------------------------------
+{- | A Floyd-Hoare triple is of the form 
+
+        { P }  c { Q }
+
+     where 
+      
+     - `P` and `Q` are assertions (think `BExp`) and 
+     - `c` is a command (think `Com`) 
+    
+     A Floyd-Hoare triple states that 
+
+     IF 
+
+     * The program `c` is starts at a state where the *precondition* `P` is True, and 
+     * The program finishes execution
+
+     THEN 
+
+     * At the final state, the *postcondition* `Q` will also evaluate to True.
+
+     -}
+
+{- | Lets paraphrase the following Hoare triples in English.
+
+   1) {True}   c {X = 5}
+
+   2) {X = m}  c {X = m + 5}
+
+   3) {X <= Y} c {Y <= X}
+
+   4) {True}   c {False}
+
+-}
+
+
+--------------------------------------------------------------------------------
+-- | The type `Assertion` formalizes the type for the 
+--   assertions (i.e. pre- and post-conditions) `P`, `Q`
+--   appearing in the triples {P} c {Q}
+
+type Assertion = BExp 
+
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+{- | Legitimate Triples 
+--------------------------------------------------------------------------------
+
+Which of the following triples are "legit" i.e.,  the claimed relation between 
+`pre`condition` `P`, `com`mand `C`, and `post`condition `Q` is true?
+
+   1) {True}  
+        X <~ 5 
+      {X = 5}
+
+   2) {X = 2} 
+        X <~ X + 1 
+      {X = 3}
+
+   3) {True}  
+        X <~ 5; 
+        Y <~ 0 
+      {X = 5}
+
+   4) {True}  
+        X <~ 5; 
+        Y <~ X 
+      {Y = 5}
+
+   5) {X = 2 && X = 3} 
+        X <~ 5 
+      {X = 0}
+
+   6) {True} 
+        SKIP 
+      {False}
+
+   7) {False} 
+        SKIP 
+      {True}
+
+   8) {True} 
+        WHILE True DO 
+          SKIP 
+      {False}
+
+   9) {X = 0}
+        WHILE X <= 0 DO 
+          X <~ X + 1 
+      {X = 1}
+
+   10) {X = 1}
+         WHILE not (X <= 0) DO 
+           X <~ X + 1 
+       {X = 100}
+ -}
+
+--------------------------------------------------------------------------------
+-- | `Legit` formalizes the notion of when a Floyd-Hoare triple is legitimate 
+--------------------------------------------------------------------------------
+{-@ type Legit P C Q =  s:{State | bval P s} 
+                     -> s':_ -> Prop (BStep C s s') 
+                     -> {bval Q s'} 
+  @-}
+type Legit = State -> State -> BStep -> Proof 
+
+-- | {True}  X <~ 5  {X = 5} ---------------------------------------------------
+
+{-@ leg1 :: Legit tt (Assign {"x"} (N 5)) (Equal (V {"x"}) (N 5)) @-}
+leg1 :: Legit  
+leg1 s s' (BAssign {}) 
+  = S.lemma_get_set "x" 5 s 
+
+
+-- | {True}  X <~ 5; y <- X  {X = 5} -------------------------------------------
+
+{-@ leg3 :: Legit tt (Seq (Assign {"x"} (N 5)) (Assign {"y"} (V {"x"}))) (Equal (V {"y"}) (N 5)) @-}
+leg3 :: Legit  
+leg3 s s' (BSeq _ _ _ smid _ (BAssign {}) (BAssign {})) 
+  = S.lemma_get_set "x" 5 s &&& S.lemma_get_set "y" 5 smid 
+
+
+-- | {False}  X <~ 5  {X = 0} --------------------------------------------------
+
+{-@ leg5 :: Legit ff (Assign {"x"} (N 5)) (Equal (V {"x"}) (N 22)) @-}
+leg5 :: Legit  
+leg5 s s' _ = () 
+
+
+--------------------------------------------------------------------------------
+-- | Two simple facts about Floyd-Hoare Triples --------------------------------
+--------------------------------------------------------------------------------
+
+{-@ lem_post_true :: p:_ -> c:_ -> Legit p c tt @-}
+lem_post_true :: Assertion -> Com -> Legit
+lem_post_true p c = \s s' c_s_s' -> () 
+
+{-@ lem_pre_false :: c:_ -> q:_ -> Legit ff c q @-}
+lem_pre_false :: Com -> Assertion -> Legit 
+lem_pre_false c q = \s s' c_s_s' -> () 
+
+
+-- | Assignment 
+
+--  { Y = 1     }  X <~ Y      { X = 1 }
+
+--  { X + Y = 1 }  X <~ X + Y  { X = 1 }
+
+--  { a = 1     }  X <~ a      { X = 1 }
+
+
+{- | Lets fill in the blanks
+
+     { ??? } 
+        x <~ 3 
+     { x == 3 }
+
+     { ??? } 
+        x <~ x + 1 
+     { x <= 5 }
+
+     { ??? }
+        x <~ y + 1 
+     { 0 <= x && x <= 5 }
+
+ -} 
+
+
+{- | To conclude that an arbitrary postcondition `Q` holds after 
+     `x <~ a`, we need to assume that Q holds before `x <~ a` 
+     but with all occurrences of `x` replaced by `a` in `Q` 
+
+     Lets revisit the example above:
+
+     { ??? } 
+        x <~ 3 
+     { x == 3 }
+
+     { ??? } 
+        x <~ x + 1 
+     { x <= 5 }
+
+     { ??? }
+        x <~ y + 1 
+     { 0 <= x && x <= 5 }
+
+  -} 
+
+--------------------------------------------------------------------------------
+-- | `Valid`ity of an assertion
+--------------------------------------------------------------------------------
+
+
+-- forall s. bval P s == True 
+{-@ type Valid P = s:State -> { v: Proof | bval P s } @-}
+type Valid = State -> Proof 
+
+-- x >= 0 || x < 0
+
+{-@ checkValid :: p:_ -> Valid p -> () @-}
+checkValid :: Assertion -> Valid -> ()
+checkValid p v = () 
+
+-- x <= 0 
+ex0 = checkValid (e0 `bImp` e1) (\_ -> ())
+  where 
+    e0 = (V "x") `Leq` (N 0)
+    e1 = ((V "x") `Minus` (N 1)) `Leq` (N 0)
+
+-- x <= 0 => x - 1 <= 0
+-- e1 = e0 `bImp` ((V "x" `Minus` N 1) `Leq` (N 0))
+
+--------------------------------------------------------------------------------
+-- | When does an assertion `Imply` another
+--------------------------------------------------------------------------------
+
+{-@ type Imply P Q = Valid (bImp P Q) @-}
+
+-- 10 <= x => 5 <= x
+{-@ v1 :: _ -> Imply (Leq (N 10) (V {"x"})) (Leq (N 5) (V {"x"})) @-} 
+v1 :: a -> Valid 
+v1 _ = \_ -> ()
+
+-- (0 < x && 0 < y) ===> (0 < x + y)
+{-@ v2 :: _ -> Imply (bAnd (Leq (N 0) (V {"x"})) (Leq (N 0) (V {"y"}))) 
+                     (Leq (N 0) (Plus (V {"x"}) (V {"y"})))
+  @-}             
+v2 :: a -> Valid 
+v2 _ = \_ -> ()
+
+--------------------------------------------------------------------------------
+-- | The Floyd-Hoare proof system
+--------------------------------------------------------------------------------
+
+data FHP where 
+  FH :: Assertion -> Com -> Assertion -> FHP
+
+data FH where 
+  FHSkip    :: Assertion -> FH 
+  FHAssign  :: Assertion -> Vname -> AExp -> FH 
+  FHSeq     :: Assertion -> Com -> Assertion -> Com -> Assertion -> FH -> FH -> FH 
+  FHIf      :: Assertion -> Assertion -> BExp -> Com -> Com -> FH -> FH -> FH
+  FHWhile   :: Assertion -> BExp -> Com -> FH -> FH 
+  FHConPre  :: Assertion -> Assertion -> Assertion -> Com -> Valid -> FH -> FH 
+  FHConPost :: Assertion -> Assertion -> Assertion -> Com -> FH -> Valid -> FH 
+
+{-@ data FH where 
+      FHSkip   :: p:_
+               -> Prop (FH p Skip p) 
+    | FHAssign :: q:_ -> x:_ -> a:_
+               -> Prop (FH (bsubst x a q) (Assign x a) q) 
+    | FHSeq    :: p:_ -> c1:_ -> q:_ -> c2:_ -> r:_ 
+               -> Prop (FH p c1 q) 
+               -> Prop (FH q c2 r) 
+               -> Prop (FH p (Seq c1 c2) r) 
+    | FHIf     :: p:_ -> q:_ -> b:_ -> c1:_ -> c2:_
+               -> Prop (FH (bAnd p b)       c1 q) 
+               -> Prop (FH (bAnd p (Not b)) c2 q)
+               -> Prop (FH p (If b c1 c2) q)
+    | FHWhile  :: inv:_ -> b:_ -> c:_
+               -> Prop (FH (bAnd inv b) c inv) 
+               -> Prop (FH inv (While b c) (bAnd inv (Not b)))
+    | FHConPre :: p':_ -> p:_ -> q:_ -> c:_  
+               -> Imply p' p
+               -> Prop (FH p c q) 
+               -> Prop (FH p' c q)
+    | FHConPost :: p:_ -> q:_ -> q':_ -> c:_  
+                -> Prop (FH p c q) 
+                -> Imply q q'
+                -> Prop (FH p c q')
+  @-}
+
+--------------------------------------------------------------------------------
+-- | THEOREM: Soundness of Floyd-Hoare Logic 
+--------------------------------------------------------------------------------
+-- thm_fh_legit :: p:_ -> c:_ -> q:_ -> Prop (FH p c q) -> Legit p c q
+
+-- thm_legit_fh :: p:_ -> c:_ -> q:_ -> Legit p c q -> Prop (FH p c q) 
+
+
+--------------------------------------------------------------------------------
+-- | Making FH Algorithmic: Verification Conditions 
+--------------------------------------------------------------------------------
+data ICom 
+  = ISkip                          -- skip 
+  | IAssign Vname     AExp         -- x := a
+  | ISeq    ICom      ICom         -- c1; c2
+  | IIf     BExp      ICom  ICom   -- if b then c1 else c2
+  | IWhile  Assertion BExp  ICom   -- while {I} b c 
+  deriving (Show)
+
+{-@ reflect pre @-}
+pre :: ICom -> Assertion -> Assertion 
+pre ISkip          q = q
+pre (IAssign x a)  q = bsubst x a q 
+pre (ISeq c1 c2)   q = pre c1 (pre c2 q)
+pre (IIf b c1 c2)  q = bIte b (pre c1 q) (pre c2 q) 
+pre (IWhile i _ _) _ = i 
+
+
+
+
+{-@ reflect vc @-}
+vc :: ICom -> Assertion -> Assertion
+vc ISkip          _ = tt 
+vc (IAssign {})   _ = tt 
+vc (ISeq c1 c2)   q = (vc c1 (pre c2 q)) `bAnd` (vc c2 q)
+vc (IIf _ c1 c2)  q = (vc c1 q) `bAnd` (vc c2 q)
+vc (IWhile i b c) q = ((bAnd i b)       `bImp` (pre c i)) `bAnd`   -- { i && b} c { i }
+                      ((bAnd i (Not b)) `bImp` q        ) `bAnd`   -- { i & ~b} => Q 
+                      vc c i
+
+{-@ reflect erase @-}
+erase :: ICom -> Com 
+erase ISkip          = Skip 
+erase (IAssign x a)  = Assign x a 
+erase (ISeq c1 c2)   = Seq (erase c1) (erase c2)
+erase (IIf b c1 c2)  = If b (erase c1) (erase c2)
+erase (IWhile _ b c) = While b (erase c)
+
+-----------------------------------------------------------------------------------
+-- | THEOREM: Soundness of VC
+-----------------------------------------------------------------------------------
+-- thm_vc :: c:_ -> q:_ -> Valid (vc c q) -> Legit (pre c q) (erase c) q
+
+-----------------------------------------------------------------------------------
+-- | Extending the above to triples [HW] 
+-----------------------------------------------------------------------------------
+
+{-@ reflect vc' @-}
+vc' :: Assertion -> ICom -> Assertion -> Assertion 
+vc' p c q = bAnd (bImp p (pre c q)) (vc c q) 
+
+-----------------------------------------------------------------------------------
+-- | THEOREM: Soundness of VC'
+-----------------------------------------------------------------------------------
+-- thm_vc' :: p:_ -> c:_ -> q:_ -> Valid (vc' p c q) -> Legit p (erase c) q
+
+