Richard, Ranjit,
Thanks for providing your solutions.
--
Alexander.
On 8 December 2014 at 21:45, Ranjit Jhala
Dear Alexander,
FWIW, this sort of thing is quite straightforward with LiquidHaskell:
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1418064183.hs
or, the code below:
-----
{-@ LIQUID "--no-termination" @-}
module Nat255 where
-- | Define a predicate for valid integers
{-@ predicate IsValid X = 0 <= X && X < 255 @-}
-- | Use the predicate to define a refinement type (subset) of valid integers
{-@ type Valid = {v:Int | IsValid v} @-}
-- | A function that checks whether a given Int is indeed valid
{-@ isValid :: n:Int -> {v:Bool | Prop v <=> IsValid n} @-} isValid n = 0 <= n && n < (255 :: Int)
-- | A function that can only be called with Valid Ints.
{-@ workWithValidNumber :: Valid -> IO () @-} workWithValidNumber n = putStrLn $ "This is a valid number" ++ show (n :: Int)
-- | This is fine... ok = workWithValidNumber 12
-- | ... But this is not. notOk = workWithValidNumber 257
-- | Finally the top level loop that inputs a number, tests it -- and calls `workWithValidNumber` if the number is valid.
loop = do putStrLn "Enter Number between 0 and 255" n <- readLn :: IO Int if isValid n then workWithValidNumber n else putStrLn "Humph, bad input, try again!" >> loop
-- Alexander