Skip to content

Semantic expression specification

Jim Weirich edited this page May 25, 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
  Given(:one)     { Number.new(1) }
  Given(:two)     { Number.new(2) }
  Given(:three)   { Number.new(3) }
  Given(:four)    { Number.new(4) }
  Given(:five)    { Number.new(5) }
  Given(:ten)     { Number.new(10) }
  Given(:hundred) { Number.new(100) }

  Given(:initial_env) { { y: hundred } }

  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) { five }
    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(:initial_env) { { x: four } }
      When(:result) { expr.reduce(initial_env) }
      let(:reduced_expression)  { result[0].inspect }
      let(:reduced_environment) { result[1] }

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

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

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

      Invariant { reduced_environment == initial_env }

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

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

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

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

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

      Invariant { reduced_environment == initial_env }

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

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

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

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

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

      Invariant { reduced_environment == initial_env }

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

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

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

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

describe "Statements" do
  Given(:zero)    { Number.new(0) }
  Given(:one)     { Number.new(1) }
  Given(:two)     { Number.new(2) }
  Given(:three)   { Number.new(3) }
  Given(:five)    { Number.new(5) }
  Given(:hundred) { Number.new(100) }

  Given(:initial_env) { { y: hundred } }

  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(:stmt) { Assign.new(:x, five) }

    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: five) }
    end
  end

  describe If do
    Given(:left)        { zero }
    Given(:right)       { one }
    Given(:condition)   { LessThan.new(left, right) }
    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(initial_env) }
      let(:reduced_statement)   { result[0].inspect }
      let(:reduced_environment) { result[1] }

      Invariant { reduced_environment == initial_env }

      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(: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(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: one) }
      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 While do
    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(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

describe Machine do
  Given(:one)    { Number.new(1) }
  Given(:two)    { Number.new(2) }
  Given(:three)  { Number.new(3) }
  Given(:four)   { Number.new(4) }
  Given(:five)   { Number.new(5) }
  Given(:six)    { Number.new(6) }
  Given(:twelve) { Number.new(12) }

  Given(:mul12) { Multiply.new(one, two) }
  Given(:mul34) { Multiply.new(three, four) }

  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 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: twelve}] }
    end

    context "where we loop" do
      Given(:varx)        { Variable.new(:x) }
      Given(:condition)   { LessThan.new(varx, five) }
      Given(:body)        { Assign.new(:x, Add.new(varx, two)) }
      Given(:expression)  { While.new(condition, body) }
      Given(:initial_env) { { x: four } }

      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: four } || env == { x: six } } }
    end
  end
end