From: ts Date: 2000-09-12T20:06:08+09:00 Subject: [ruby-talk:4891] [TOY] FL I've written this small module, just to play with ruby. It has probably many bugs and probably work only with this example, this is *really* only a toy :-) pigeon% cat b.rb #!/usr/bin/ruby require 'fl' class A < FL def invariant puts "invariant class A" super end def alpha(x, y) pre { @old = {} print "pre alpha : ", y, "\n" @old['first'] = x } post { |result| print "post alpha : ", x, " -- ", result.join(' -- '), "\n" } 1 + 1 end end class B < A def invariant puts "invariant class B" super end def alpha(a, b) print "old value : ", @old['first'], "\n" if a == 1 puts "if true" return [3, 4] end puts "void return" [1, 2] end end a = B.new puts "=======> alpha" p a.alpha(1, 4) puts "=======> alpha" p a.alpha(2, 4) pigeon% pigeon% b.rb =======> alpha invariant class B invariant class A pre alpha : 4 old value : 1 if true post alpha : 1 -- 3 -- 4 invariant class B invariant class A [3, 4] =======> alpha invariant class B invariant class A pre alpha : 4 old value : 2 void return post alpha : 2 -- 1 -- 2 invariant class B invariant class A [1, 2] pigeon% :-) Guy Decoux