Permalink
Browse files

Added VerProg, for programs with verified postconditions

  • Loading branch information...
1 parent 022015a commit 3b14e79d566555d299656996497e186ee8bd7138 Edwin Brady committed May 26, 2011
Showing with 28 additions and 13 deletions.
  1. +11 −0 ResIO.idr
  2. +17 −13 safe-file.idr
View
@@ -147,6 +147,13 @@ data ResProg : Set -> Set where
RP : {xs':Vect ResTy n} ->
ResIO a (O,clear n) (t,xs') -> ResProg a;
+data VerProg : (n:Nat) -> (Vect ResTy n -> Set) -> Set -> Set where
+ VP : {xs':Vect ResTy n} ->
+ {P:Vect ResTy n -> Set} ->
+ ResIO a (O, clear n) (t, xs') ->
+ P xs' ->
+ VerProg n P a;
+
clearEnv : (n:Nat) -> ResEnv (clear n);
clearEnv O = Empty;
clearEnv (S k) = Extend II (clearEnv k);
@@ -155,6 +162,10 @@ run : ResProg a -> IO a;
run (RP {n} (ResIOp f)) = do { cenv' <- f (clearEnv n);
return (fst cenv'); };
+vrun : {P:Vect ResTy n -> Set} -> VerProg n P a -> IO a;
+vrun {n} (VP (ResIOp f) p) = do { cenv' <- f (clearEnv n);
+ return (fst cenv'); };
+
resources = intToNat;
}
View
@@ -64,19 +64,23 @@ do using (BIND, RETURN) {
readFile : ResSub (FILE (Open Reading)) String;
readFile h = CALL (readFile' "") h;
- test : ResProg ();
- test = RP {n=resources 1}
- do { open "Test" Reading fO;
- h <- GET fO;
- CHECK h (LIFT (putStrLn "File open error"))
- (do { h <- GET fO;
- content <- CALL readFile h;
- LIFT (putStrLn content);
- close h;
- return II;
- });
- };
+ data AllClosed : Vect ResTy n -> Set where
+ ClosedNil : AllClosed VNil
+ | ClosedMore : {xs:Vect ResTy n} ->
+ AllClosed xs -> AllClosed (RTy (FILE Closed) :: xs);
+
+ test : VerProg (resources 1) AllClosed ();
+ test = VP do { open "Test" Reading fO;
+ h <- GET fO;
+ CHECK h (LIFT (putStrLn "File open error"))
+ (do { h <- GET fO;
+ content <- CALL readFile h;
+ LIFT (putStrLn content);
+ close h;
+ return II;
+ });
+ } (ClosedMore ClosedNil);
}
-main = run test;
+main = vrun test;

0 comments on commit 3b14e79

Please sign in to comment.