Skip to content

Programming at the specification level

Alberto edited this page Mar 29, 2017 · 11 revisions

What you have below is the complete realization (except low level calls) for an Automatic Teller Machine, using the language haskell and the package Transient, following the written requrements here:

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

The specification were made originally to exemplify how to make it in Java, following the standard workflow of Object Oriented Programming.

My implementation demonstrates that it is possible to program at the specification level. It follows closely the structure of the specification and his language, so it is clear enough to be understood by the client and the maintainers without the need of documentation.

The program can be run in a server and a web browser or in a console with little modifications.

The point is that each one of the inputs is asynchronous. wlink is a link in a web page (it could be a control in a GUI or a input in a console). The code look so simple that it is hard to realize it. Moreover the code of the example includes the code of the browser AND the server.

In a usual programming you should rely on events and global state. or else, multithreading with inter-process communication. That is the point. Look at the document linked at the end.

Compare this with the great quantity of code and documentation that are necessary for all the program lifecycle using an OOP language like Java (you can find them in the above link)

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

For a detailed discussion about why this implementation is so concise and close the specification and why this is impossible using conventional software techniques, see the inital paragraphs of this:

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

There I advanced the problems and the solutions some time ago.

Communications with the server in the low level primitives are not present, but it is quite straightforward using Transient and would not break the flow, but it would add additional complications in a conventional framework.

The implementation of the ATM:

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