Skip to content

Semantic expression specification

Jim Weirich edited this page May 24, 2013 · 9 revisions

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

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

describe "Expressions" do
  Invariant { expr.inspect == #{expr}»" }
  Invariant {
    expr.reducible? == ! [Number, Bool].include?(expr.class)
  }
  Invariant { expr.reducible?.implies expr.respond_to?(:reduce_expression) }
  Invariant {
    (! expr.reducible?).implies {
      lambda { expr.reduce({}) }.should raise_error(/not reducible/i)
    }
  }

  describe Number do
    Given(:expr) { Number.new(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" do
      Given(:four) { Number.new(4) }
      Given(:original_env) { { x: four } }
      When(:result) { expr.reduce(original_env) }
      let(:reduced_expression)  { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Then { reduced_expression == "«4»" }
      Then { reduced_environment == original_env }
    end
  end

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

    describe "#reduce" do
      Given(:reducible) { Add.new(Number.new(1), Number.new(2)) }
      When(:result) { expr.reduce({}) }
      let(:reduced_expression)  { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Invariant { reduced_environment == {} }

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

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

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

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

    describe "#reduce" do
      Given(:reducible) { Add.new(Number.new(1), Number.new(2)) }
      When(:result) { expr.reduce({}) }
      let(:reduced_expression)  { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Invariant { reduced_environment == {} }

      context "where the nothing is reducible" do
        Given(:expr) { Multiply.new(Number.new(2), Number.new(3)) }
        Then { reduced_expression == "«6»" }
      end

      context "where the left is reducible" do
        Given(:expr) { Multiply.new(reducible, Number.new(10)) }
        Then { reduced_expression == "«3 * 10»" }
      end

      context "where the right is reducible" do
        Given(:expr) { Multiply.new(Number.new(10), reducible) }
        Then { reduced_expression == "«10 * 3»" }
      end
    end
  end

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

    describe "#reduce" do
      Given(:reducible) { Add.new(Number.new(1), Number.new(2)) }
      When(:result) { expr.reduce({}) }
      let(:reduced_expression)  { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Invariant { reduced_environment == {} }

      context "where the result is true" do
        Given(:expr) { LessThan.new(Number.new(2), Number.new(3)) }
        Then { reduced_expression == "«true»" }
      end

      context "where the result is false" do
        Given(:expr) { LessThan.new(Number.new(4), Number.new(3)) }
        Then { reduced_expression == "«false»" }
      end

      context "where the left is reducible" do
        Given(:expr) { LessThan.new(reducible, Number.new(10)) }
        Then { reduced_expression == "«3 < 10»" }
      end

      context "where the right is reducible" do
        Given(:expr) { LessThan.new(Number.new(10), reducible) }
        Then { reduced_expression == "«10 < 3»" }
      end
    end
  end
end

describe "Statements" do
  Invariant { stmt.inspect == #{stmt}»" }
  Invariant {
    stmt.reducible? == ! stmt.is_a?(DoNothing)
  }

  describe DoNothing do
    Given(:stmt) { DoNothing.new }
    Then { stmt.to_s == "do-nothing" }
    Then { stmt == DoNothing.new }
    Then { stmt != Variable.new(:x) }
  end

  describe Assign do
    Given(:five) { Number.new(5) }
    Given(:stmt) { Assign.new(:x, five) }
    Then { stmt.to_s == "x = 5" }
    Then { stmt != DoNothing.new }
    Then { stmt == Assign.new(:x, five) }

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

      Then { reduced_statement == "«do-nothing»" }
      Then { reduced_environment ==  {x: five} }
    end
  end

  describe If do
    Given(:zero) { Number.new(0) }
    Given(:one) { Number.new(1) }
    Given(:a) { zero }
    Given(:b) { one }
    Given(:condition) { LessThan.new(a, b) }
    Given(:consequence) { Assign.new(:x, zero) }
    Given(:alternative) { Assign.new(:x, one) }
    Given(:stmt) { If.new(condition, consequence, alternative) }

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

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

      Invariant { reduced_environment == { } }

      context "where condition is reducible" do
        Then { reduced_statement == "«if (true) { x = 0 } else { x = 1 }»" }
      end

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

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

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

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

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

    describe "#reduce" do
      When(:result) { stmt.reduce({}) }
      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 == { x: one } }
      end

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

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

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

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

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

describe Machine do
  Given(:one)   { Number.new(1) }
  Given(:two)   { Number.new(2) }
  Given(:three) { Number.new(3) }
  Given(:four)  { Number.new(4) }
  Given(:mul12)  { Multiply.new(one, two) }
  Given(:mul34)  { Multiply.new(three, four) }

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

    context "where we add and multiply" do
      Given(:expression) { Add.new(mul12, mul34) }
      Then { result.inspect == "«14»" }
      Then {
        steps == [
          "«1 * 2 + 3 * 4»",
          "«2 + 3 * 4»",
          "«2 + 12»",
          "«14»"
        ]
      }
      Then { envs.all? { |env| env == {} } }
    end

    context "where we compare" do
      Given(:expression) { LessThan.new(two, mul34) }
      Then { result.inspect == "«true»" }
      Then {
        steps == [
          "«2 < 3 * 4»",
          "«2 < 12»",
          "«true»"
        ]
      }
      Then { envs.all? { |env| env == {} } }
    end

    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: Number.new(12)}] }
    end
  end
end