Example Feature Requirements
Let us consider the following simplistic requirements to an order processing feature of a typical e-commerce application:- There is a stock of products.
- Each product in stock is counted in whole numbers.
- An order is a set of products with their respective quantities.
- An order can be accepted for processing only if there is enough stock of all ordered products.
- Orders are processed in the order they are submitted.
- Processing an order means decreasing the stock quantities of respective products.
VDM-SL
VDM is based on the concept of refinement: Starting with a top level abstract specification and then gradually refining (adding details to) types and functions.VDM-SL used for examples is based on lambda-calculus, thus essentially is a statically typed functional language, in contrast to its extensions: VDM++ for object-oriented and VDM-RT for real-time applications.
We shall consider three levels of refinement:
- Abstract specification.
- Detailed specification with implicitly defined functions - what they do, not how.
- Detailed specification with explicitly defined functions so that they can be executed with VDM-SL interpreter.
The abstract specification defines only key data types and signatures of functions - the data flow.
-- Top level data and flow outline
types
Product = token;
Quantity = nat1;
ProductSpec = map Product to Quantity;
Stock = ProductSpec;
Order = ProductSpec;
Operations ::
Stock
seq of Order
inv mk_Operations(stock, orders) == let consolidatedOrders = consolidate(orders) in
forall product in set dom consolidatedOrders &
product in set dom stock
and consolidatedOrders(product) <= stock(product);
functions
consolidate(specs: seq of ProductSpec) consolidatedSpec: ProductSpec == undefined;
checkOut(op: Operations, order: Order) op': Operations == undefined;
processOrder(op: Operations) op': Operations == undefined;
Remarks:
- We use token type for something we do not want to or need to specify at given level of abstraction.
- We can provide invariant for data types with inv expression.
- We keep all the functions undefined to start with - relying on type signatures only.
Our first refinement is to define the key functions - checkOut and processOrder - implicitly, i.e. by specifying their pre-condition and, more importantly, post-condition, which essentially is the definition of what the function does.
-- Refined impclicit specification
types
Product = token;
Quantity = nat1;
ProductSpec = map Product to Quantity;
Stock = ProductSpec;
Order = ProductSpec;
Operations ::
Stock
seq of Order
inv mk_Operations(stock, orders) == let consolidatedOrders = consolidate(orders) in
forall product in set dom consolidatedOrders &
product in set dom stock
and consolidatedOrders(product) <= stock(product);
functions
consolidate(specs: seq of ProductSpec) consolidatedSpec: ProductSpec == undefined;
checkOut(op: Operations, order: Order) op': Operations
pre orderProductsAreValid(op, order) and thereIsEnoughStock(op, order)
post let
mk_Operations(stock, orders) = op,
mk_Operations(stock', orders') = op' in
stock' = stock -- stock was not changed
and orders' = orders ^ [order]; -- order was appended to the list of orders
orderProductsAreValid(op: Operations, order: Order) result: bool == undefined; -- self descriptve
thereIsEnoughStock(op: Operations, order: Order)result: bool == undefined; -- self descriptve
processOrder(op: Operations) op': Operations
post let
mk_Operations(stock, orders) = op,
mk_Operations(stock', orders') = op',
theOrder = hd orders in
orders' = tl orders -- processed order was removed
and forall product in set dom theOrder &
stock'(product) = stock(product) - theOrder(product); -- stock quantities were decreased
Remarks:
- We may also keep some secondary functions undefined for the time being.
Next step is to provide all functions with their explicit bodies that can be effectively evaluated, thus interpreted with, e.g. the Overture Tool.
-- Refined explicit (executable) specification
types
Product = <vanilla> | <chocolate> | <strawberry>; -- token refined into a set of quotes
Quantity = nat1;
ProductSpec = map Product to Quantity;
Stock = ProductSpec;
Order = ProductSpec;
Operations ::
Stock
seq of Order
inv mk_Operations(stock, orders) == let consolidatedOrders = consolidate(orders) in
forall product in set dom consolidatedOrders &
product in set dom stock
and consolidatedOrders(product) <= stock(product);
functions
consolidate(specs: seq of ProductSpec) consolidatedSpec: ProductSpec == consolidateRec({|->}, specs);
consolidateRec(consodilatedSpec: ProductSpec, specs: seq of ProductSpec) consolidatedSpec: ProductSpec ==
if specs = [] then
consodilatedSpec
else
let theSpec = hd specs in
consolidateRec(consodilatedSpec
++ {p |-> consodilatedSpec(p) + theSpec(p) | p in set dom theSpec}, tl specs);
checkOut(op: Operations, order: Order) op': Operations == let mk_Operations(stock, orders) = op in
mk_Operations(stock, orders ^ [order]) -- keep the stock and add the order
pre orderProductsAreValid(op, order) and thereIsEnoughStock(op, order);
orderProductsAreValid(op: Operations, order: Order) result: bool == let mk_Operations(stock, -) = op in
dom order subset dom stock;
thereIsEnoughStock(op: Operations, order: Order)result: bool == let mk_Operations(stock, -) = op in
forall product in set dom order & order(product) <= stock(product);
processOrder(op: Operations) op': Operations ==
let
mk_Operations(stock, orders) = op,
theOrder = hd orders in
-- decrease the stock
mk_Operations(stock ++ {p |-> stock(p) - theOrder(p) | p in set dom theOrder}, tl orders)
pre let mk_Operations(-, orders) = op in len orders > 0;
test() result : bool == processOrder(
checkOut(
mk_Operations({<vanilla> |-> 10, <chocolate> |-> 10, <strawberry> |-> 10}, []),
{<vanilla> |-> 5, <chocolate> |-> 7}
)
) = mk_Operations({<vanilla> |-> 5, <chocolate> |-> 3, <strawberry> |-> 10}, []);Remarks:
- We converted implicit post-conditions into function bodies - in complex cases, we may keep post-conditions as a way to verify the explicit implementation.
- We provided a small test function that calls checkOut and processOrder then verifies the result.
Haskell
Below is an implementation of the above specification in Haskell.module Main where
import qualified Data.Map as Map
data Product = Vanilla | Chocolate | Strawberry
deriving (Eq, Ord)
type Quantity = Int
type ProductSpec = Map.Map Product Quantity
type Stock = ProductSpec
type Order = ProductSpec
data Operations = Operations Stock [Order]
deriving Eq
type Error = String
checkOut :: Operations -> Order -> Either Operations Error
checkOut op@(Operations stock orders) order = if not (orderProductsAreValid op order)
then Right "Some of the products are not in stock"
else if not (thereIsEnoughStock op order)
then Right "Not enough stock"
else Left $ Operations stock (orders ++ [order])
orderProductsAreValid :: Operations -> Order -> Bool
orderProductsAreValid op@(Operations stock _) order = all (\p -> Map.member p stock) (Map.keys order)
thereIsEnoughStock :: Operations -> Order -> Bool
thereIsEnoughStock op@(Operations stock _) order = all (\p -> (order Map.! p) <= (stock Map.! p)) (Map.keys order)
processOrder :: Operations -> Operations
processOrder op@(Operations stock (theOrder : restOfOrders)) = Operations (foldl updateStock stock (Map.keys theOrder)) restOfOrders
where
updateStock :: ProductSpec -> Product -> ProductSpec
updateStock stock product = Map.update (\_ -> Just $ (stock Map.! product) - (theOrder Map.! product)) product stock
processOrder op@(Operations _ []) = op
test = testProcessOrder (checkOut (Operations (Map.fromList [(Vanilla, 10), (Chocolate, 10), (Strawberry, 10)]) [])
(Map.fromList [(Vanilla, 5), (Chocolate, 7)]))
where
testProcessOrder (Left ops) = processOrder ops == (Operations (Map.fromList [(Vanilla, 5), (Chocolate, 3), (Strawberry, 10)]) [])
testProcessOrder (Right _) = False
main = putStrLn $ show test
Remarks:
- The code is very similar, data type definitions are almost identical - the translation is straightforward.
- VDSM-SL version in many ways is more abstract and easy to read, e.g. compare
dom order subset dom stock
expression with the Haskell analogall (\p -> Map.member p stock) (Map.keys order) - We had to deal with error handling in Haskell instead of simply relying on the pre-condition in checkOut.
F#
Similarly, below is an implementation of the above specification in F#.type Product = Vanilla | Chocolate | Strawberry
type Quantity = int
type ProductSpec = Map
type Stock = ProductSpec
type Order = ProductSpec
type Operations = {stock: Stock; orders: Order list}
exception OrderProcessing of string
let orderProductsAreValid {stock = stock} order =
Map.forall (fun product _ -> Map.containsKey product stock) order
let thereIsEnoughStock {stock = stock} order =
Map.forall (fun product _ -> (Map.find product stock) >= (Map.find product order)) order
let checkOut ops order =
if orderProductsAreValid ops order && thereIsEnoughStock ops order
then { ops with orders = List.append ops.orders [order] }
else raise (OrderProcessing "Incorrect order")
let processOrder {stock = stock; orders = orders} =
let order = List.head orders
let updateStock stock product quantity = Map.add product (Map.find product stock - Map.find product order) stock
in {stock = Map.fold updateStock stock order; orders = List.tail orders}
let test =
let initialOps = {stock = Map.ofList [(Vanilla, 10); (Chocolate, 10); (Strawberry, 10)]; orders = []}
let order = Map.ofList [(Vanilla, 5); (Chocolate, 7)]
let expectedOps = {stock = Map.ofList [(Vanilla, 5); (Chocolate, 3); (Strawberry, 10)]; orders = []}
in checkOut initialOps order |> processOrder = expectedOps
try
printfn "%b" test
with
| OrderProcessing message -> printfn "Error: %s" message
Remarks:
- The code is also very similar, thus easy to translate.
- We opted for exceptions for error handling, thus the signature of checkOut was kept the same as in the specification.
Conclusions
We believe, this small example shows that VDM style refinement is a pragmatic tool for requirements analysis in the correct-by-construction approach to software development.Particularly, VDM-SL fits nicely as the design language in between requirements analysis and an implementation in a functional programming language.
