An online auctioneer

Members register, list items and bid. Each auction closes at the closing time its seller chose. The highest bidder pays, the seller is paid less the platform’s service fee, the item is shipped and the buyer rates the sale.

The model shows how far delegation carries a specification. Its use cases state their requirements in prose, as a client would, and each requirement is met by the lower-level service the process requests. Thus the formal URDAD-OCL is written once, on the services which keep the members, the listings and the sales, and the method’s progress report confirms that every use-case condition is met by delegation.

The model verifies with no errors even at the executable level, and its leaf services state their answers precisely enough for an execution environment to give them without any code. It keeps six warnings, each with a written reason.