Invariant and Failure Modes

Some Expressions and Statements are Reducible ...

... but others aren't.

In the small-step semantics model, each AST is reduced one step at a time, producing a new reduced AST. This continues until it produces an AST that cannot be reduced.

Here are the steps for reducing an expression like «2 * 3 + 4»:

expr = Add.new(Multiply.new(Number.new(2), Number.new(3)), Number.new(4))
expr                                # => «2 * 3 + 4»
expr = expr.reduce_expression({})   # => «6 + 4»
expr = expr.reduce_expression({})   # => «10»
expr.class                          # => Number

At this point the expression is reduced as far as it can go. The final expression is a Number, which is irreducible. Number and Bool expressions, along with DoNothing statements are also irreducible.

Calling :reduce_expression on on that final expr is undefined and would be erroneous. The programmer is supposed to check :reducible? before calling :reduce_expression or :reduce. However, as a quality of implementation issue, we would like to specify that calling :reduce_expression on irreducible expressions (and :reduce on statements) fails with an exception.

We can capture that intent with an invariant.

describe "Expressions" do
  Invariant {
    (! expr.reducible?).implies {
      lambda { expr.reduce_expression({}) }.should raise_error(/not reducible/i)
    }
  }

  describe Number do
    Given(:expr) { Number.new(5) }
    ...
  end

  describe Bool do
    Given(:expr) { Bool.new(false) }
    ...
  end

  describe Variable do
    Given(:expr) { Variable.new(:x) }
    ...
  end
  ...
end

describe "Statements" do
  Invariant {
    (! stmt.reducible?).implies {
      lambda { stmt.reduce({}) }.should raise_error(/not reducible/i)
    }
  }

  describe DoNothing do 
    Given(:stmt) { DoNothing.new }
    ...
  end

  describe Assign do
    Given(:stmt) { Assign.new(:x, Number.new(3)) }
    ...
  end
  ...
end

Note that we are using :implies in the invariant assertions. :implies is not supplied with the Ruby language, so we have to roll our own. You can see the details on the Implies Implementation page.

---

Return to Semantic Expression Examples