Skip to content

Programming at the specification level

Alberto edited this page Jun 22, 2016 · 11 revisions

What you have below is the (almost) complete realization, using haskell and Transient, of the specification for an Automatic Teller Machine, following the written specification here:

http://www.math-cs.gordon.edu/courses/cs211/ATMExample/

The specification were made originally to exemplify how to program it in Java following the standard workflow of OOP.

This example demonstrate how it is possible to program at the user requirement level. The program follows closely the specifications and is clear enough to be understood by the client and the maintainers without the help of profuse documentation. Since the program derives directly from the specification and uses little more than the specification nomenclature, except in very low level details.

Compare this with the great quantity of files of code and documentation necessary for the design, implementation and documentation of the application that are necessary for his usage an maintenance.

The full source code with the haskell headers are at: https://github.com/agocorona/transient/blob/master/examples/Atm.hs

For a detailed discussion about why this implementation is so concise and close the specification see the iniital paragraphs of this:

https://www.schoolofhaskell.com/user/agocorona/EDSL-for-hard-working-IT-programmers#the-problem--parallelization--concurrency-and-inversion-of-control

main= initNode atm

atm= do
   card <- waitCard
   pin <- enterPIN
   validateBank pin card
   setData card
   performTransactions <|> cancel
   returnCard

performTransactions = do
    clearScreen
    operation <- withdrawal <|> deposit <|> transfer <|> balanceInquiry
    printReceipt operation
    return ()

withdrawal= do
    wlink ()  $ toElem "withdrawall"
    wprint "choose bank account"
    account <- chooseAccount
    wprint "Enter the quantity"
    quantity <- getInt Nothing
    if quantity `rem` 20 /= 0
      then do
        wprint "multiples of $20.00 please"
        stop
      else do
        r <- approbalBank account quantity
        case r of
            False -> do
                wprint "operation denied. sorry"
                wprint "Another transaction?"
                r <- wlink True (b "yes ") <|> wlink False << (b "No")
                if not r then return ()
                                 else performTransactions
            True  ->  giveMoney r

deposit= do
    wlink () $ b "Deposit "
    wprint "choose bank account"
    account <- chooseAccount
    r <- approbalBankDeposit account
    case r of
        False -> do wprint "operation denied. sorry"
                    stop
        True  -> do
            r <- waitDeposit <|> timeout
            case r of
                False -> do wprint "timeout, sorry"; stop
                True  -> return ()

transfer= do
    wlink () $ b "Transfer "
    wprint "From"
    ac <- chooseAccount
    wprint "amount"
    amount <- inputDouble Nothing
    wprint "To"
    ac' <- chooseAccount
    transferAccBank ac ac' amount
    return()

balanceInquiry= do
    wprint "From"
    ac <- chooseAccount
    r <- getBalanceBank ac
    wprint $ "balance= "++ show r

validateBank pin card = atServer $ validate' pin card (0 :: Int)
   where
   validate' pin card times= local $ do
    r <- verifyPinBank pin card
    if r then return () else do
     if times ==2
      then do
        wprint ("three tries. card will be retained" :: String)
        stop

      else validate' pin card $ times + 1

rtotal= unsafePerformIO $ newEmptyMVar
ractive= unsafePerformIO $ newMVar False

switchOnOff= on <|> off
  where
  on= do
     wbutton () "On"
     wprint "enter total amount of money"
     total <- getInt Nothing
     liftIO $ do
       tryTakeMVar rtotal
       putMVar rtotal total
  off= do
     wbutton () "Off"
     active <- liftIO $ readMVar ractive
     if active then stop else wprint "ATM stopped"

type AccountNumber= String
newtype Card= Card [AccountNumber]  deriving Typeable

waitCard = local $ render $ wbutton Card "enter card"

enterPIN= local $ do
      wprint "Enter PIN"
      render $ getInt Nothing `fire` OnChange

cancel= wbutton () "Cancel"

returnCard= wprint "Card returned"

clearScreen=  wraw $ forElems "body" $ this >> clear


printReceipt= do
    Operation str <- getSData <|> error "no operation"
    wprint $ "receipt: Operation:"++ str

chooseAccount= do
    Card accounts <- getSData <|> error "transfer: no card"
    wprint "choose an account"
    mconcat[wlink ac (fromStr $ ' ':show ac) | ac <- accounts]

approbalBank ac quantity= return True

giveMoney n= wprint $ "Your money : " ++ show n ++ " Thanks"

approbalBankDeposit ac= return True

transferAccBank ac ac' amount= wprint $ "transfer from "++show ac ++ " to "++show ac ++ " done"

getBalanceBank ac= liftIO $ do
    r <- rand
    return $ r * 1000

verifyPinBank _ _= liftIO $ do
    liftIO $ print "verifyPinBank"
    r <- rand
    if r > 0.2 then return True else return False

waitDeposit = do
     n <- liftIO rand
     if n > 0.5 then return True else return False

rand:: IO Double
rand= randomRIO

timeout t= threadDelay $ t * 1000000
Clone this wiki locally