Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

PSM Framework Example

  • Local search can be represented in the following operational specification:

  • operational specification local search
      output := local search(input);
      local search(X)
        begin
          currents := select1(X);
          output := recursion(currents);
        end
      recursion(X)
        begin
        successors := generate(X);
        new := select2(X, successors);
          if X = new
          then output := select3(X);
          else recursion(new);
        end



    select1(x) ⊆ x


    x ∈ generate(y) ↔ x ∈ input ∧ ∃z.(z ∈ y ∧ successor(z, x))


    select2(y, y’) ⊆ y ∪ y’


    ¬∃x, z . (z ∈ (y ∪ y’) \ select2(y, y’) ∧ x < z)
    y ∪ y’ ≠ ∅ → ∃x.(x ∈ select2(y, y’))


    select3(y) ⊆ y


    ¬∃x, z . (z ∈ (y \ select3(y)) ∧ x ∈ select3(y)
    ∧ x < z)
    y ≠ ∅ → ∃x.(x ∈ select3(y))
    endoperational spec


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.