From: Bernhard Brodowsky Date: 2010-04-28T01:42:13+09:00 Subject: Re: Formal methods Robert Dober wrote: > On Sat, Apr 17, 2010 at 12:08 AM, Bernhard Brodowsky > >> 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. :D -- Posted via http://www.ruby-forum.com/.