-
Notifications
You must be signed in to change notification settings - Fork 28
Programming at the specification level
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:
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
| Intro
| How-to
| Backtracking to undo IO actions and more
| Finalization: better than exceptions
| Event variables: Publish Suscribe
| Checkpoints(New), suspend and restore
| Remote execution: The Cloud monad
| Clustering: programming the cloud
| Mailboxes for cloud communications
| Distributed computing: map-reduce