VDM-SL Example: Order Processing

This post takes an example of a trivial order processing feature to demonstrate how Vienna Development Method (VDM) can be utilized as the requirements analysis and solution design method matching functional languages for implementation perfectly.

Example Feature Requirements

Let us consider the following simplistic requirements to an order processing feature of a typical e-commerce application:

1. There is a stock of products.
2. Each product in stock is counted in whole numbers.
3. An order is a set of products with their respective quantities.
4. An order can be accepted for processing only if there is enough stock of all ordered products.
5. Orders are processed in the order they are submitted.
6. 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:

1. Abstract specification.
2. Detailed specification with implicitly defined functions - what they do, not how.
3. Detailed specification with explicitly defined functions so that they can be executed with VDM-SL interpreter.

Abstract Specification
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:

1. We use token type for something we do not want to or need to specify at given level of abstraction.
2. We can provide invariant for data types with inv expression.
3. We keep all the functions undefined to start with - relying on type signatures only.

Implicit Specification
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:

1. We may also keep some secondary functions undefined for the time being.

Explicit Specification
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:

1. We converted implicit post-conditions into function bodies - in complex cases, we may keep post-conditions as a way to verify the explicit implementation.
2. 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:

1. The code is very similar, data type definitions are almost identical - the translation is straightforward.
2. 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 analog
   
   

   all (\p -> Map.member p stock) (Map.keys order)

3. 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:

1. The code is also very similar, thus easy to translate.
2. 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.