Prev: transfer GBK into UTF-8 in csv file
Next: [ANN] PDF::Writer officially retired in favor of Prawn
From: Bernhard Brodowsky on 15 Apr 2010 10:43
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?
--
Posted via http://www.ruby-forum.com/.

From: Caleb Clausen on 16 Apr 2010 13:40
On 4/15/10, Bernhard Brodowsky <brodowsb(a)student.ethz.ch> 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.

From: Bernhard Brodowsky on 16 Apr 2010 18:08
Caleb Clausen wrote:
> On 4/15/10, Bernhard Brodowsky <brodowsb(a)student.ethz.ch> 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.
--
Posted via http://www.ruby-forum.com/.

From: Caleb Clausen on 16 Apr 2010 19:18
On 4/16/10, Bernhard Brodowsky <brodowsb(a)student.ethz.ch> wrote:
> Caleb Clausen wrote:
>> On 4/15/10, Bernhard Brodowsky <brodowsb(a)student.ethz.ch> 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.

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.

From: Robert Dober on 17 Apr 2010 11:42
On Sat, Apr 17, 2010 at 12:08 AM, Bernhard Brodowsky
<brodowsb(a)student.ethz.ch> <snip>
> 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 best way to predict the future is to invent it.
-- Alan Kay

 |  Next  |  Last
Pages: 1 2 3
Prev: transfer GBK into UTF-8 in csv file
Next: [ANN] PDF::Writer officially retired in favor of Prawn