Prev: transfer GBK into UTF-8 in csv file
Next: [ANN] PDF::Writer officially retired in favor of Prawn
From: Robert Dober on 27 Apr 2010 12:58
On Tue, Apr 27, 2010 at 6:42 PM, Bernhard Brodowsky
<brodowsb(a)student.ethz.ch> wrote:
> Robert Dober wrote:
<snip>
> Maybe I'll do my bachelor thesis on this. :D
To re insist on the complexity of the thing, PhD you mean?
;)
R.

--
The best way to predict the future is to invent it.
-- Alan Kay

From: Bernhard Brodowsky on 27 Apr 2010 12:42
Robert Dober wrote:
> 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 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/.

From: William Rutiser on 27 Apr 2010 16:04
Robert Dober wrote:
> On Tue, Apr 27, 2010 at 6:42 PM, Bernhard Brodowsky
> <brodowsb(a)student.ethz.ch> wrote:
>
>> Robert Dober wrote:
>>
> <snip>
>
>> Maybe I'll do my bachelor thesis on this. :D
>>
> To re insist on the complexity of the thing, PhD you mean?
> ;)
> 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



From: Robert Dober on 27 Apr 2010 19:24
On Tue, Apr 27, 2010 at 10:04 PM, William Rutiser
<wruyahoo05(a)comcast.net> wrote:
> Robert Dober wrote:
>>
>> On Tue, Apr 27, 2010 at 6:42 PM, Bernhard Brodowsky
>> <brodowsb(a)student.ethz.ch> wrote:
>>
>>>
>>> Robert Dober wrote:
>>>
>>
>> <snip>
>>
>>>
>>> Maybe I'll do my bachelor thesis on this. :D
>>>
>>
>> To re insist on the complexity of the thing, PhD you mean?
>> ;)
>> R.
>
<snip>
I guess you did not really read the thread, did you? OP insisted to
prove general Ruby Programs, 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.



--
The best way to predict the future is to invent it.
-- Alan Kay

From: Robert Klemme on 29 Apr 2010 05:22
2010/4/27 Bernhard Brodowsky <brodowsb(a)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/

First  |  Prev  |  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