Semantic expression specification

Full Semantic Expression Specification

This is the full specification that I've been playing with, captured in a moment of time. The examples from the Semantic Expression Examples page are extracted (and simplified) from the following code.

# -*- coding: utf-8 -*-

require 'rspec/given'
require 'semantics'

RSpec::Given.use_natural_assertions


# Helper classes and methods -------------------------------------------

class FalseClass
  def implies(consequent=false)
    true
  end
end

class NilClass
  def implies(consequent=false)
    true
  end
end

class Object
  def implies(consequent=false)
    if block_given?
      yield
    else
      consequent
    end
  end
end

def num(number)
  Number.new(number)
end


# Expressions ----------------------------------------------------------

describe "Expressions" do
  Given(:initial_env) { { y: num(100) } }

  Invariant { expr.inspect == "«#{expr}»" }
  Invariant {
    expr.reducible? != [Number, Bool].include?(expr.class)
  }
  Invariant {
    (! expr.reducible?).implies {
      expect { expr.reduce_expression({}) }.to raise_error(/not reducible/i)
    }
  }

  describe Number do
    Given(:expr) { num(5) }
    Then { expr.to_s == "5" }
  end

  describe Bool do
    Given(:expr) { Bool.new(true) }
    Then { expr.to_s == "true" }
  end

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

    Then { expr.to_s == "x" }

    describe "#reduce_expression" do
      Given(:initial_env) { { x: num(4) } }
      When(:result) { expr.reduce_expression(initial_env) }

      Then { result.inspect == "«4»" }
    end
  end

  describe Add do
    Given(:expr) { Add.new(num(2), num(3)) }
    Then { expr.to_s == "2 + 3" }

    describe "#reduce_expression" do
      Given(:reducible) { Add.new(num(1), num(2)) }
      When(:result) { expr.reduce_expression(initial_env) }

      context "where the nothing is reducible" do
        Given(:expr) { Add.new(num(2), num(3)) }
        Then { result.inspect == "«5»" }
      end

      context "where the left is reducible" do
        Given(:expr) { Add.new(reducible, num(10)) }
        Then { result.inspect == "«3 + 10»" }
      end

      context "where the right is reducible" do
        Given(:expr) { Add.new(num(10), reducible) }
        Then { result.inspect == "«10 + 3»" }
      end
    end
  end

  # NOTE: The remaining binary operators share a common
  # implementation, so need less extensive checking.

  describe Subtract do
    Given(:expr) { Subtract.new(num(3), num(2)) }
    Then { expr.to_s == "3 - 2" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }
      Then { result.inspect == "«1»" }
    end
  end

  describe Multiply do
    Given(:expr) { Multiply.new(num(2), num(3)) }
    Then { expr.to_s == "2 * 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }
      Then { result.inspect == "«6»" }
    end
  end

  describe Divide do
    Given(:expr) { Divide.new(num(6), num(2)) }
    Then { expr.to_s == "6 / 2" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }
      Then { result.inspect == "«3»" }
    end
  end

  describe EqualTo do
    Given(:expr) { EqualTo.new(num(2), num(3)) }
    Then { expr.to_s == "2 == 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { EqualTo.new(num(2), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left > right" do
        Given(:expr) { EqualTo.new(num(4), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left == right" do
        Given(:expr) { EqualTo.new(num(3), num(3)) }
        Then { result.inspect == "«true»" }
      end
    end
  end

  describe NotEqualTo do
    Given(:expr) { NotEqualTo.new(num(2), num(3)) }
    Then { expr.to_s == "2 != 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { NotEqualTo.new(num(2), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left > right" do
        Given(:expr) { NotEqualTo.new(num(4), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left == right" do
        Given(:expr) { NotEqualTo.new(num(3), num(3)) }
        Then { result.inspect == "«false»" }
      end
    end
  end

  describe LessThan do
    Given(:expr) { LessThan.new(num(2), num(3)) }
    Then { expr.to_s == "2 < 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { LessThan.new(num(2), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left > right" do
        Given(:expr) { LessThan.new(num(4), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left == right" do
        Given(:expr) { LessThan.new(num(3), num(3)) }
        Then { result.inspect == "«false»" }
      end
    end
  end

  describe LessThanOrEqualTo do
    Given(:expr) { LessThanOrEqualTo.new(num(2), num(3)) }
    Then { expr.to_s == "2 <= 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { LessThanOrEqualTo.new(num(2), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left > right" do
        Given(:expr) { LessThanOrEqualTo.new(num(4), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left == right" do
        Given(:expr) { LessThanOrEqualTo.new(num(3), num(3)) }
        Then { result.inspect == "«true»" }
      end
    end
  end

  describe GreaterThan do
    Given(:expr) { GreaterThan.new(num(2), num(3)) }
    Then { expr.to_s == "2 > 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { GreaterThan.new(num(2), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left > right" do
        Given(:expr) { GreaterThan.new(num(4), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left == right" do
        Given(:expr) { GreaterThan.new(num(3), num(3)) }
        Then { result.inspect == "«false»" }
      end
    end
  end

  describe GreaterThanOrEqualTo do
    Given(:expr) { GreaterThanOrEqualTo.new(num(2), num(3)) }
    Then { expr.to_s == "2 >= 3" }

    describe "#reduce_expression" do
      When(:result) { expr.reduce_expression(initial_env) }

      context "where left < right" do
        Given(:expr) { GreaterThanOrEqualTo.new(num(2), num(3)) }
        Then { result.inspect == "«false»" }
      end

      context "where left > right" do
        Given(:expr) { GreaterThanOrEqualTo.new(num(4), num(3)) }
        Then { result.inspect == "«true»" }
      end

      context "where left == right" do
        Given(:expr) { GreaterThanOrEqualTo.new(num(3), num(3)) }
        Then { result.inspect == "«true»" }
      end
    end
  end
end


# Statements -----------------------------------------------------------

describe "Statements" do
  Given(:initial_env) { { y: num(100) } }

  Invariant { stmt.inspect == "«#{stmt}»" }
  Invariant {
    stmt.reducible? == ! stmt.is_a?(DoNothing)
  }
  Invariant {
    (! stmt.reducible?).implies {
      expect { stmt.reduce({}) }.to raise_error(/not reducible/i)
    }
  }

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

    Then { stmt.to_s == "do-nothing" }
    Then { stmt == DoNothing.new }
    Then { stmt != Assign.new(:x, num(5)) }
  end

  describe Assign do
    Given(:stmt) { Assign.new(:x, num(5)) }

    Then { stmt.to_s == "x = 5" }

    describe "#reduce" do
      When(:result) { stmt.reduce(initial_env) }
      let(:reduced_statement)   { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Then { reduced_statement == "«do-nothing»" }
      Then { reduced_environment ==  initial_env.merge(x: num(5)) }
    end
  end

  describe Sequence do
    Given(:first)  { Assign.new(:x, num(1)) }
    Given(:second) { Assign.new(:y, num(1)) }
    Given(:stmt)   { Sequence.new(first, second) }

    Then { stmt.to_s == "x = 1; y = 1" }

    describe "#reduce" do
      When(:result) { stmt.reduce(initial_env) }
      let(:reduced_statement)   { result[0].inspect }
      let(:reduced_environment) { result[1] }

      context "where first statement is reducible" do
        Then { reduced_statement == "«do-nothing; y = 1»" }
        Then { reduced_environment == initial_env.merge(x: num(1)) }
      end

      context "where first statement is not reducible" do
        Given(:first) { DoNothing.new }
        Then { reduced_statement == "«y = 1»" }
        Then { reduced_environment == initial_env }
      end
    end
  end

  describe If do
    Given(:condition)   { Bool.new(true) }
    Given(:consequence) { Assign.new(:x, num(0)) }
    Given(:alternative) { Assign.new(:x, num(1)) }
    Given(:stmt)        { If.new(condition, consequence, alternative) }

    Then { stmt.to_s == "if (true) { x = 0 } else { x = 1 }" }

    describe "#reduce" do
      When(:result) { stmt.reduce(initial_env) }
      let(:reduced_statement)   { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Invariant { reduced_environment == initial_env }

      context "where condition is reducible" do
        Given(:condition)   { LessThan.new(num(0), num(1)) }
        Then { reduced_statement == "«if (true) { x = 0 } else { x = 1 }»" }
      end

      context "where condition is non-reducible true" do
        Given(:condition) { Bool.new(true) }
        Then { reduced_statement == "«x = 0»" }
      end

      context "where condition is non-reducible false" do
        Given(:condition) { Bool.new(false) }
        Then { reduced_statement == "«x = 1»" }
      end
    end
  end

  describe While do
    Given(:xvar)      { Variable.new(:x) }
    Given(:condition) { LessThan.new(xvar, num(3)) }
    Given(:body)      { Assign.new(:x, Add.new(xvar, num(2))) }
    Given(:stmt)      { While.new(condition, body) }

    Then { stmt.to_s == "while (x < 3) { x = x + 2 }" }

    describe "#reduce" do
      When(:result) { stmt.reduce(initial_env) }
      let(:reduced_statement)   { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Then {
        reduced_statement == (
          "«if (x < 3) { x = x + 2; " +
          "while (x < 3) { x = x + 2 } " +
          "} else { do-nothing }»")
      }
      Then { reduced_environment == initial_env }
    end
  end
end


# Virtual Machine ------------------------------------------------------

describe Machine do
  Given(:mul12) { Multiply.new(num(1), num(2)) }
  Given(:mul34) { Multiply.new(num(3), num(4)) }

  Given(:initial_env) { {} }

  describe "#reduce" do
    let(:steps) { [] }
    let(:envs)  { [] }
    Given(:mach) {
      Machine.new(expression, initial_env) do |exp, env|
        steps << exp.inspect
        envs  << env
      end
    }
    When(:result) { mach.run }

    context "where we assign" do
      Given(:expression) { Assign.new(:x, mul34) }
      Then { result.inspect == "«do-nothing»" }
      Then {
        steps == [
          "«x = 3 * 4»",
          "«x = 12»",
          "«do-nothing»"
        ]
      }
      Then { envs == [{}, {}, {x: num(12)}] }
    end

    context "where we loop" do
      Given(:varx)        { Variable.new(:x) }
      Given(:condition)   { LessThan.new(varx, num(5)) }
      Given(:body)        { Assign.new(:x, Add.new(varx, num(2))) }
      Given(:expression)  { While.new(condition, body) }
      Given(:initial_env) { { x: num(4) } }

      Then { result.inspect == "«do-nothing»" }
      Then {
        steps == [
          "«while (x < 5) { x = x + 2 }»",
          "«if (x < 5) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«if (4 < 5) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«if (true) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«x = x + 2; while (x < 5) { x = x + 2 }»",
          "«x = 4 + 2; while (x < 5) { x = x + 2 }»",
          "«x = 6; while (x < 5) { x = x + 2 }»",
          "«do-nothing; while (x < 5) { x = x + 2 }»",
          "«while (x < 5) { x = x + 2 }»",
          "«if (x < 5) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«if (6 < 5) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«if (false) { x = x + 2; while (x < 5) { x = x + 2 } } else { do-nothing }»",
          "«do-nothing»",
        ]
      }
      Then { envs.all? { |env| env == { x: num(4) } || env == { x: num(6) } } }
    end
  end
end