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