From: Robert Klemme <shortcutter@...>
Date: 2010-04-29T18:22:10+09:00
Subject: Re: Formal methods

2010/4/27 Bernhard Brodowsky <brodowsb@student.ethz.ch>:

> The thing is, that I'm still somewhat suspicious if it's really
> impossible.

For practical purposes the difference between "impossible" and "takes
500 man years" might be negligible. :-)

Just a small demonstration: how do you prove that method test() below
does not invoke a method on nil?

Ruby version 1.9.1
irb(main):001:0> def test(x)
irb(main):002:1> if x.nil?
irb(main):003:2> puts "no calling!"
irb(main):004:2> else
irb(main):005:2* x.boom!
irb(main):006:2> end
irb(main):007:1> end
=> nil
irb(main):008:0> test nil
no calling!
=> nil
irb(main):009:0> class NilClass; def nil?; false; end; end
=>
irb(main):010:0> test nil
/opt/lib/ruby19/1.9.1/irb/slex.rb:234:in `match_io': undefined method
`call' for nil:NilClass (NoMethodError)
        from /opt/lib/ruby19/1.9.1/irb/slex.rb:75:in `match'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:287:in `token'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:263:in `lex'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:234:in `block (2
levels) in each_top_level_statement'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:230:in `loop'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:230:in `block in
each_top_level_statement'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:229:in `catch'
        from /opt/lib/ruby19/1.9.1/irb/ruby-lex.rb:229:in
`each_top_level_statement'
        from /opt/lib/ruby19/1.9.1/irb.rb:153:in `eval_input'
        from /opt/lib/ruby19/1.9.1/irb.rb:70:in `block in start'
        from /opt/lib/ruby19/1.9.1/irb.rb:69:in `catch'
        from /opt/lib/ruby19/1.9.1/irb.rb:69:in `start'
        from /opt/bin/irb19:12:in `<main>'

It seems that since you have no control over the code and not even
over the types of objects passed to methods you probably have to
include the complete code of a program (i.e. including standard
library in Ruby and C) in your formal reasoning.  While this may be
possible the question is how long does it take and what do we gain by
this?

> I mean, if I write a program, I know what a certain method
> does. It's not that I write something and just hope that the
> nondeterministic Ruby does something useful, but I really am able to
> make correct programs. (Of course, I make mistakes, but that's something
> else, I just mean that I DO usually know, what a method does)

Writing a program and even testing that it works correctly is a
totally difference category of problem than proving that the program
has particular properties (e.g. that it terminates, see
http://en.wikipedia.org/wiki/Halting_problem).

> And I think if it is possible to understand Ruby code, it should be
> possible to formalize this. Even though it is very difficult.
>
> All this understandings of my code are based on assumptions. I only know
> that the method does what it is supposed to do, because I assume that
> the arithmetic used in this method works correctly and the objects
> passed to this method fulfill certain conditions, for example, have a
> certain method that does what I need from this object.

But you cannot assume that an instance passed to a method will
reliably respond to an arbitrary method.  The fact that in Ruby
variables are typeless means that you can make zero assumptions about
a method argument unless you prove your way up the call chain.

> Like this, you should be able to find preconditions. Of course, in Ruby
> it is not sufficient to use things like "a has to be positive" as a
> precondition, but much more expressive ones like "a has to be an object
> which has a method foo and this method foo has to do exactly the same
> like my code in method foo".

Something like that, yes - and probably also how what method behaves.

> Of course, this is still far far away from formal methods, but I just
> cannot believe that I actually do understand all my programs (well, most
> of them, you know what I mean) but that it's not possible to prove them
> formally.
>
> Maybe I'll do my bachelor thesis on this. :D

Could be that the prove that proving is impossible for Ruby can be
easier than the prove that a particular program is correct. :-)

Good luck!

Kind regards and greetings to your professor

robert

-- 
remember.guy do |as, often| as.you_can - without end
http://blog.rubybestpractices.com/