Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
-- syntax of While type Var = String --type Num = Integer data Aexp = Var Var | Num Integer | Aexp :+ Aexp | Aexp :- Aexp | Aexp :* Aexp data Bexp = T | F | Aexp :== Aexp | Aexp :<= Aexp | Not Bexp | Bexp :&& Bexp | Bexp :|| Bexp data Stm = Var := Aexp | Skip | Stm :\ Stm | If Bexp Stm Stm | While Bexp Stm data AbsInt = NoInt | Zero | Neg | Pos | NonZero | NonNeg | NonPos | AnyInt deriving (Eq, Show) absint :: Integer -> AbsInt absint x | x == 0 = Zero | x < 0 = Neg | x > 0 = Pos instance Num AbsInt where NoInt + i = NoInt AnyInt + i = AnyInt Zero + i = i Neg + Neg = Neg i + Zero = i Neg + Pos = AnyInt i + AnyInt = AnyInt Pos + Neg = AnyInt Pos + Pos = Pos -- NoInt - i = NoInt Neg - Pos = Neg AnyInt - i = AnyInt Pos - Pos = AnyInt data AbsBool = NoBool | TT | FF | AnyBool deriving (Eq, Show) absbool :: Bool -> AbsBool absbool True = TT absbool False = FF -- class Lattice a where join :: a -> a -> a bottom :: a instance Lattice AbsInt where NoInt `join` x = x x `join` NoInt = x AnyInt `join` x = AnyInt Pos `join` Pos = Pos Neg `join` Neg = Neg bottom = NoInt instance Lattice AbsBool where NoBool `join` x = x x `join` NoBool = x TT `join` FF = AnyBool bottom = NoBool instance Lattice b => Lattice (a -> b) where (f `join` g) x = f x `join` g x bottom x = bottom -- semantic categories for direct style denotational semantics type State = Var -> Integer allzeros :: State allzeros x = 0 type AbsState = Var -> AbsInt allanys :: AbsState allanys x = AnyInt allnones :: AbsState allnones x = NoInt update :: Eq a => (a -> b) -> a -> b -> (a -> b) update st y z x = if x == y then z else st x cond :: (State -> Bool, State -> State, State -> State) -> (State -> State) cond (pred, g1, g2) st = if pred st then g1 st else g2 st abscond :: (AbsState -> AbsBool, AbsState -> AbsState, AbsState -> AbsState) -> (AbsState -> AbsState) abscond (pred, g1, g2) st = case pred st of NoBool -> allnones TT -> g1 st FF -> g2 st AnyBool -> g1 st `join` g2 st fix :: (a -> a) -> a fix f = f (fix f) fixappr :: (Lattice a, Eq a) => (a -> a) -> a --fix :: ((State -> State) -> (State -> State)) -> (State -> State) fixappr f = fixappr' f bottom fixappr' :: (Lattice a, Eq a) => (a -> a) -> a -> a fixappr' f a = let a' = f a in if a' == a then a else fixappr' f a' instance Eq a => Eq (Var -> a) where f == g = f "x" == g "x" && f "y" == g "y" && f "z" == g "z" -- direct style denotational semantics -- -- arithmetical expressions semA :: Aexp -> State -> Integer semA (Var x) st = st x semA (Num n) st = n semA (a1 :+ a2) st = semA a1 st + semA a2 st semA (a1 :- a2) st = semA a1 st - semA a2 st semA (a1 :* a2) st = semA a1 st * semA a2 st abssemA :: Aexp -> AbsState -> AbsInt abssemA (Var x) st = st x abssemA (Num n) st = absint n abssemA (a1 :+ a2) st = abssemA a1 st + abssemA a2 st abssemA (a1 :- a2) st = abssemA a1 st - abssemA a2 st abssemA (a1 :* a2) st = abssemA a1 st * abssemA a2 st -- -- boolean expressions semB :: Bexp -> State -> Bool semB T st = True semB F st = False semB (a1 :== a2) st = semA a1 st == semA a2 st semB (a1 :<= a2) st = semA a1 st <= semA a2 st semB (Not b) st = not (semB b st) semB (b1 :&& b2) st = semB b1 st && semB b2 st semB (b1 :|| b2) st = semB b1 st || semB b2 st abssemB :: Bexp -> AbsState -> AbsBool abssemB T st = TT abssemB F st = FF abssemB (a1 :== a2) st = case (abssemA a1 st, abssemA a2 st) of (NoInt, _) -> NoBool (Pos, Neg) -> FF (Pos, Zero) -> FF (Pos, Pos) -> AnyBool (AnyInt, _) -> AnyBool (_, AnyInt) -> AnyBool (Zero, Zero) -> TT (Neg, Zero) -> FF --abssemB (a1 :<= a2) st = abssemA a1 st <= abssemA a2 st abssemB (Not b) st = case abssemB b st of NoBool -> NoBool TT -> FF FF -> TT AnyBool -> AnyBool --abssemB (b1 :&& b2) st = abssemB b1 st && abssemB b2 st --abssemB (b1 :|| b2) st = abssemB b1 st || abssemB b2 st -- -- statements dssemS :: Stm -> State -> State dssemS (x := a) st = update st x (semA a st) dssemS Skip st = st dssemS (s1 :\ s2) st = (dssemS s2 . dssemS s1) st dssemS (If b s1 s2) st = cond (semB b, dssemS s1, dssemS s2) st dssemS (While b s) st = fix f st where f g = cond (semB b, g . dssemS s, id) dsabssemS :: Stm -> AbsState -> AbsState dsabssemS (x := a) st = update st x (abssemA a st) dsabssemS Skip st = st dsabssemS (s1 :\ s2) st = (dsabssemS s2 . dsabssemS s1) st dsabssemS (If b s1 s2) st = abscond (abssemB b, dsabssemS s1, dsabssemS s2) st {- dsabssemS (While b s) st = fixappr f st where f g = abscond (abssemB b, g . dsabssemS s, id) -} dsabssemS (While b s) st = fixappr f where f st' = (case abssemB b st' of NoBool -> allnones TT -> dsabssemS s st' FF -> allnones AnyBool -> dsabssemS s st') `join` st -- example {- fact is abstract syntax for y := 1 ; while not (x = 1) do (y := y + x ; x := x - 1) -} --fact :: Stm fact = ("y" := Num 1) :\ (While (Not (Var "x" :== Num 0)) (("y" := (Var "y" :+ Var "x")) :\ ("x" := (Var "x" :- Num 1)) ) ) testfact :: AbsInt -> (AbsInt, AbsInt) testfact z = (st' "x", st' "y") where st' = dsabssemS fact st where st = update allanys "x" z