require: preconditions in production code
The complete source of testing_require.ek9, compiled by the EK9 compiler. Shown on testing.html.
#!ek9 defines module site.testing.require defines type OrderStatus Created Submitted defines record OrderItem sku as String: String() quantity as Integer: Integer() OrderItem() as pure -> sku as String quantity as Integer this.sku :=? sku this.quantity :=? quantity default operator ? defines class Order customerId as String: String() items as List of OrderItem: List() status as OrderStatus: OrderStatus.Created //Constructor with preconditions - if these fail, the caller has a bug Order() -> customerId as String initialItems as List of OrderItem require customerId? require initialItems is not empty this.customerId: customerId items += initialItems //Method with preconditions addItem() -> item as OrderItem require item? require status == OrderStatus.Created items += item //Method ensuring an invariant submit() require items is not empty require status == OrderStatus.Created status: OrderStatus.Submitted default operator ? defines program OrderLifecycle() stdout <- Stdout() order <- Order("customer-7", [OrderItem("widget", 2)]) order.addItem(OrderItem("gadget", 1)) order.submit() stdout.println("Order submitted")
Output
Order submitted