improve 0.0.7 → 0.0.8

raw patch · 4 files changed

+136/−8 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +131/−5
• Language/ImProve/Core.hs +2/−0
• Language/ImProve/Verify.hs +1/−1
• improve.cabal +2/−2

@@ -1,3 +1,128 @@+{- |+ImProve is an imperative programming language for high assurance applications.++ImProve uses infinite state, unbounded model checking to verify programs+adhere to specifications, which are written in the form of assertion statements.+If it is unable to verify an assertion, ImProve will emit a counter example+that shows a precise program trace that exercises the assertion violation.++The following compares the syntax of C and ImProve:++/Variable Declarations/++@+float a = 0.0;            a <- 'float' \"a\" 0+bool b = true;            b <- 'bool' \"b\" true+int c = d + e + 3;        c <- 'int'' \"c\" (d + e + 3)+@++/Variable Assignments/++@+a = 1;                    a '<==' 1+@++/Conditional Statements/++@+if (condition) {          'if_' condition $ do +    a();                      a+    b();                      b+    c();                      c+}++if (condition {           'ifelse' condition+    a();                      (do a+    b();                          b+    c();                          c)+}                             (do d+else {                            e +    d();                          f)+    e();+    f();+}                                 +@++/Assertion Statements/++@+assert(condition);        'assert' condition+@++/Statement Labels/++@+hello: {                  'label' \"hello\" $ do+    a();                      a+    b();                      b+}+@++/Expressions/++@+/Constant Literals/++true                      'true'+false                     'false'+0                         0+100                       100+1.0                       1     -- float+3.14                      3.14++/Variable Reference/++a                         'ref' a++/Logical Expressions/++! a                       'not_' a+a && b                    a '&&.' b+a || b                    a '||.' b++/Comparison Expressions/++a == b                    a '==.' b+a != b                    a '/=.' b+a < b                     a '<.' b+a > b                     a '>.' b+a <= b                    a '<=.' b+a >= b                    a '>=.' b++/Arithmetic Expressions/++a + b                     a '+' b+a * b                     a '*.' b+a \/ b                     a '/.' b     -- float+a \/ b                     a '`div_`' b -- int+a % b                     a '`mod_`' b+abs(a)                    'abs' a+min(a, b)                 'min_' a b+max(a, b)                 'max_' a b++/Conditional Expression/++a ? b : c                 'mux' a b c+@++/Function Definitions and Function Calls/+(All ImProve functions are Haskell functions that are inlined at compile time.)++@+int add(int a, int b) {                             add :: E Int -> E Int -> E Int+  return a + b;                                     add a b = a + b+}++three = add(1, 2);                                  three <== add 1 2++void incrCounter(int *counter, int amount) {        incrCounter :: V Int -> E Int -> Stmt ()+  *counter = *counter + amount;                     incrCounter counter amount = counter <== ref counter + amount+}++incrCounter(&counter, 22);                          incrCounter counter 22+@++-} module Language.ImProve   (   -- * Types@@ -11,7 +136,6 @@   , true   , false   , constant-  , zero   -- ** Variable Reference   , ref   -- ** Logical Operations@@ -59,7 +183,7 @@   , float'   , input   -- ** Variable Assignment-  , (<==)+  , Assign (..)   -- ** Conditional Execution   , ifelse   , if_@@ -204,7 +328,7 @@   slope = (y2 - y1) / (x2 - x1)   inter = y1 - slope * x1 --- | References a variable.+-- | References a variable to be used in an expression ('E'). ref :: AllE a => V a -> E a ref = Ref @@ -224,7 +348,8 @@   put (path0, stmt1)   return a --- | Labels a statement.  Useful for requirement trace tags or other annotations.+-- | Labels a statement.  Labels are used in counter examples to trace the program execution.+--   And assertion names, and hence counter example file names, are produce from labels. label :: Name -> Stmt a -> Stmt a label name stmt = do   (path0, stmt0) <- get@@ -316,7 +441,8 @@ evalStmt :: [Name] -> Stmt () -> ([Name], Statement) evalStmt path (Stmt f) = snd $ f (path, Null) -class    Assign a     where (<==) :: V a -> E a -> Stmt ()+class Assign a where+  (<==) :: V a -> E a -> Stmt () instance Assign Bool  where a <== b = statement $ AssignBool  a b instance Assign Int   where a <== b = statement $ AssignInt   a b instance Assign Float where a <== b = statement $ AssignFloat a b

@@ -21,6 +21,7 @@  type Path = [Name] +-- | A mutable variable. data V a = V Bool [Name] a deriving Eq  class    PathName a         where pathName :: a -> String@@ -48,6 +49,7 @@ instance NumE Int instance NumE Float +-- | A logical, arithmetic, comparative, or conditional expression. data E a where   Ref   :: AllE a => V a -> E a   Const :: AllE a => a -> E a

@@ -87,7 +87,7 @@  -- | Trim all unneeded stuff from a program. trimProgram :: Statement -> Statement-trimProgram program = program+trimProgram program = trim program   where   vars = fixPoint []   fixPoint :: [VarInfo] -> [VarInfo]

@@ -1,12 +1,12 @@ name:    improve-version: 0.0.7+version: 0.0.8  category: Language  synopsis: An imperative, verifiable programming language for high assurance applications.  description:-  ImProve is an imperative DSL intended for high assurance, embedded applications.+  ImProve is an imperative programming language for high assurance applications.   ImProve uses infinite state, unbounded model checking to verify programs adhere   to specifications, which are written in the form of assertion statements.   Yices (required) is the backend SMT solver.