Hi, I want to try to prove some parts of my programs formally. Does
anyone have any experience with the combination of formal methods and
Ruby?
On 4/15/10, Bernhard B. [email protected] wrote:
Hi, I want to try to prove some parts of my programs formally. Does
anyone have any experience with the combination of formal methods and
Ruby?
I don’t know much about formal methods, but my guess is that it is
very, very difficult to formally prove a ruby program. Most types of
analysis of ruby code are somewhere between very hard and actually
impossible due to the very dynamic nature of ruby. It’s because you
can change so much of the behavior of the language at runtime, so you
can’t tell until you actually are running a particular bit of code
what it might do.
Caleb C. wrote:
On 4/15/10, Bernhard B. [email protected] wrote:
Hi, I want to try to prove some parts of my programs formally. Does
anyone have any experience with the combination of formal methods and
Ruby?I don’t know much about formal methods, but my guess is that it is
very, very difficult to formally prove a ruby program. Most types of
analysis of ruby code are somewhere between very hard and actually
impossible due to the very dynamic nature of ruby. It’s because you
can change so much of the behavior of the language at runtime, so you
can’t tell until you actually are running a particular bit of code
what it might do.
It is most certainly true, that it is extremely difficult, but one has
to be ambitious some times. And actually, my formal methods professor
told me that it was difficult, but not impossible, but it depends which
properties I wanted to prove. Things like that I never call a method on
“nil” could be possible to prove according to him, so I just want to
give it a try.
On Sat, Apr 17, 2010 at 12:08 AM, Bernhard B.
[email protected]
It is most certainly true, that it is extremely difficult, but one has
to be ambitious some times. And actually, my formal methods professor
told me that it was difficult, but not impossible, but it depends which
properties I wanted to prove. Things like that I never call a method on
“nil” could be possible to prove according to him, so I just want to
give it a try.
Unless you impose severe restrictions on your program you just need to
implement a Ruby Interpreter. Even forbidding *eval does not suffice,
you would need to forbid define_method too and I am probably
forgetting something. Apart from these you need a Regexp interpreter
etc,etc.
The question is, what do you want to prove (pun intended), message
flow, properties of closure, exception handling?
Cheers
Robert
On 4/16/10, Bernhard B. [email protected] wrote:
can change so much of the behavior of the language at runtime, so you
can’t tell until you actually are running a particular bit of code
what it might do.It is most certainly true, that it is extremely difficult, but one has
to be ambitious some times. And actually, my formal methods professor
told me that it was difficult, but not impossible, but it depends which
properties I wanted to prove. Things like that I never call a method on
“nil” could be possible to prove according to him, so I just want to
give it a try.
It should be fairly easy to prove that kind of thing in some special
cases, but the general case gets hairy.
I agree that’s it’s not (quite) impossible, but… you’re definitely
headed into untrod territory. Keep me (and the list) informed of your
progress, since this would be very cool if you succeed.
PS: if you do succeed, your professor better give you a phd. No,
seriously. It’s that hard.
On Tue, Apr 27, 2010 at 6:42 PM, Bernhard B.
[email protected] wrote:
Robert D. wrote:
Maybe I’ll do my bachelor thesis on this.
To re insist on the complexity of the thing, PhD you mean?
R.
Robert D. wrote:
On Sat, Apr 17, 2010 at 12:08 AM, Bernhard B.
[email protected]It is most certainly true, that it is extremely difficult, but one has
to be ambitious some times. And actually, my formal methods professor
told me that it was difficult, but not impossible, but it depends which
properties I wanted to prove. Things like that I never call a method on
“nil” could be possible to prove according to him, so I just want to
give it a try.
Unless you impose severe restrictions on your program you just need to
implement a Ruby Interpreter. Even forbidding *eval does not suffice,
you would need to forbid define_method too and I am probably
forgetting something. Apart from these you need a Regexp interpreter
etc,etc.
The question is, what do you want to prove (pun intended), message
flow, properties of closure, exception handling?
Cheers
Robert
The thing is, that I’m still somewhat suspicious if it’s really
impossible. 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)
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.
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”.
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. 
Robert D. wrote:
R.
“Formal Methods” has meant different things to different people.
One aspect of the difference is what is to be proven. The general idea
is that some post-condition of the program’s execution is to be proven.
Its not easy to write a formal post-condition for, say, an execution of
Internet Explorer. On the other hand it may be possible to specify the
effect of some of IE’s subroutines.
Another aspect has to do with the completeness of the proof( and
specification ). For example, is it sufficient to prove that a program
gives the right answer if it doesn’t blow up or fail to terminate? Do
you need to prove those things for some pre-specified range of inputs?
Do the numbers stay inside certain hardware limits? Do numerical
round-off errors have to be considered? etc. Perhaps you can do the
proof for an abstraction of the problem, one that ignores storage
representations and other machine artifacts. Do what extent do you need
to prove the real program matches the abstraction?
A third aspect is who or what does the work. Is some tool supposed to
figure out the entire proof? or is it supposed to just check a proof
supplied by a programmer?
Fourth, does the formal method apply to an arbitrary program or only one
composed in certain limited ways?
My experience, since encountering Edsger Dijkstra circa 1970, is that it
is practical to apply his methods to some programs. I wrote the array
manipulating code for a language interpreter that way. The program was
in carefully hand optimized C, and the proofs asserted that all the
pointers were pointing where they were supposed to.
But remember that Dijkstra’s method is to write the program so that it
can be proven – almost a proof first technique.
The program text contains the assertions that must hold after each
statement. If you can’t write the assertion, and prove it follows from
previous assertions, you can’t write the statement. Note that this is an
extremely oversimplified description.
What I found was that the experience of learning to program this way had
a major effect on all my subsequent programming, even when I was not
explicitly writting down the proof steps.
Note that the details of such proofs tend to be very tedious and most of
the things to be proven are pretty trivial. What is not trivial is
breaking larger goal into such trivial steps.
I am no longer, and haven’t been for a long time, in contact with
computer science education. In particular I don’t know how much of this
is a standard part of the curriculum and how much as been discarded as
not commercially applicable.
In summary, there are at least semi-formal things that can be done and
it is very beneficial to practice doing them.
– Bill Rutiser
On Tue, Apr 27, 2010 at 10:04 PM, William R.
[email protected] wrote:
I guess you did not really read the thread, did you? OP insisted to prove general Ruby P.s, and that just means to write a Ruby Interpreter (actually a formal one, whatever that means in his context). AAMOF suggestions were made to limit verifications to certain constraints, which might have led to some more interesting discussions :(. But for some reasons that is not what he wants (sigh). Cheers R.Maybe I’ll do my bachelor thesis on this.
To re insist on the complexity of the thing, PhD you mean?
R.
2010/4/27 Bernhard B. [email protected]:
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 `’
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
Halting problem - Wikipedia).
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.
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
On 4/27/10, Bernhard B. [email protected] wrote:
The thing is, that I’m still somewhat suspicious if it’s really
impossible. 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)
You might want to look into what work has been done on formal methods
for other dynamic languages, such as lisp, scheme, or smalltalk, since
all 3 of these will present similar problems. If there’s a program
prover for lisp, there’s hope for ruby as well.