【形式化方法：VDM++系列】3.基于VDM++的图书管理系统需求定义

class Library
--类型定义
types
public Copy = token ;
public User = token ;
Borrowing = map Copy to User;

--实例定义和初始化    
instance variables
sCopies : set of Copy := {};
sUsers: set of User := {};
sBorrowing: Borrowing := { |-> };
--定义map类型实例的定义域和值域
inv 
    dom sBorrowing subset sCopies and
    rng sBorrowing subset sUsers;

operations
--定义操作，操作名add_user,输入参数类型User，返回值为空
public add_user : User ==> ()
--定义操作体，此处还尚未定义
add_user(aUser) == 
sUsers := sUsers union {aUser}
--定义操作的前置条件和后置条件
--前置条件：aUser不在sUsers中
--后置条件：aUser加入了sUsers集合
pre
    aUser not in set sUsers
post
    sUsers = sUsers~ union {aUser};

public remove_user : User ==> ()
remove_user(aUser) == 
    sUsers := sUsers \ {aUser}
pre
    aUser in set sUsers and 
    not borrowedUser(sBorrowing, aUser)
post
    sUsers = sUsers~ \ {aUser};

public add_book : Copy ==> ()
add_book(aCopy) == 
    sCopies := sCopies union {aCopy}
pre
    aCopy not in set sCopies
post
    sCopies = sCopies~ union {aCopy};

public remove_book: Copy ==> ()
remove_book(aCopy) == 
    sCopies := sCopies \ {aCopy}
pre
    aCopy in set sCopies and
    not borrowedCopy(sBorrowing, aCopy)
post
    sCopies = sCopies~ \ {aCopy};

public borrow_book : User * Copy ==> ()
borrow_book(aUser, aCopy) ==
    sBorrowing := sBorrowing munion {aCopy |-> aUser}
pre
    aUser in set sUsers and
    aCopy in set sCopies and
    not borrowedCopy(sBorrowing, aCopy)
post
    sBorrowing = sBorrowing~ munion {aCopy |-> aUser};

public return_book : Copy ==> ()
return_book(aCopy) ==
    sBorrowing := {aCopy }<-: sBorrowing
pre
    borrowedCopy(sBorrowing, aCopy)
post
    sBorrowing = {aCopy } <-: sBorrowing~;

public getAttributes : () ==> set of Copy * set of User * map Copy to User
getAttributes() == return mk_(sCopies, sUsers, sBorrowing);

functions
--函数定义，该函数判断该书是否已经被借走，输入参数是Borrowing类型和Copy类型，如果被借走则返回true
borrowedCopy : Borrowing * Copy +> bool
borrowedCopy(aBorrowing, aCopy) ==
    aCopy in set dom aBorrowing;

borrowedUser : Borrowing * User +> bool
borrowedUser(aBorrowing, aUser) ==
    aUser in set rng aBorrowing;
    
end Library

class UseLibrary

instance variables
sL : Library :=  new Library();

functions
public run : () -> seq of char * bool * map nat1 to bool
run() == 
    let testcases = [
            t1() 
        ],
        testResults = makeOrderMap(testcases)
    in
    mk_("The result of regression test = ", forall i in set inds testcases & testcases(i), testResults);

static public makeOrderMap : seq of bool +> map nat1 to bool
makeOrderMap(s) == {i |-> s(i) | i in set inds s}
pre s <> [];

operations
t1: () ==> bool
t1() == 
    let l = new Library(),
        p = mk_token("Sakoh"), 
        c = mk_token("OO Construction_1") 
    in (
        l.add_user(p); l.add_book(c); l.borrow_book(p, c); l.return_book(c); l.remove_user(p);
        return
            l.getAttributes() = mk_({mk_token("OO Construction_1")}, {}, {|->})
    );
end UseLibrary

import org.overture.codegen.runtime.*;

import java.util.*;


public class Library {
    private VDMSet sCopies = SetUtil.set();
    private VDMSet sUsers = SetUtil.set();
    private VDMMap sBorrowing = MapUtil.map();

    public Library() {
    }

    public void add_user(final Token aUser) {
        sUsers = SetUtil.union(sUsers.clone(), SetUtil.set(aUser));
    }

    public void remove_user(final Token aUser) {
        sUsers = SetUtil.diff(sUsers.clone(), SetUtil.set(aUser));
    }

    public void add_book(final Token aCopy) {
        sCopies = SetUtil.union(sCopies.clone(), SetUtil.set(aCopy));
    }

    public void remove_book(final Token aCopy) {
        sCopies = SetUtil.diff(sCopies.clone(), SetUtil.set(aCopy));
    }

    public void borrow_book(final Token aUser, final Token aCopy) {
        sBorrowing = MapUtil.munion(sBorrowing.clone(),
                MapUtil.map(new Maplet(aCopy, aUser)));
    }

    public void return_book(final Token aCopy) {
        sBorrowing = MapUtil.domResBy(SetUtil.set(aCopy), sBorrowing.clone());
    }

    public Tuple getAttributes() {
        return Tuple.mk_(sCopies.clone(), sUsers.clone(), sBorrowing.clone());
    }

    private static Boolean borrowedCopy(final VDMMap aBorrowing,
        final Token aCopy) {
        return MapUtil.dom(aBorrowing.clone()).contains(aCopy);
    }

    private static Boolean borrowedUser(final VDMMap aBorrowing,
        final Token aUser) {
        return MapUtil.rng(aBorrowing.clone()).contains(aUser);
    }
}