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")

Download testing_require.ek9

Output

Order submitted