The Artima Developer Community
Sponsored Link

Weblogs Forum
Programming with "Duh" Typing

370 replies on 25 pages. Most recent reply: Aug 8, 2007 9:54 AM by James Watson

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 370 replies on 25 pages [ « | 1 ... 21 22 23 24 25 | » ]
Petrik de Heus

Posts: 19
Nickname: p8
Registered: Jul, 2007

Re: word games Posted: Aug 2, 2007 9:56 AM
Reply to this message Reply
Advertisement
> > Is 'next' a function or a method?
> > Is 'current' a function or a method?
> > What should split do?
> > What is 'element'?
> > What is 'index'? Move the index of what?
> > Do all 3 "current"'s mean the same thing?
> > What does retrieve mean? Does the function/method
> retrieve
> > only retrieve the element from the array or does it
> also
> > return it when called?
> > How do I start it? How does it get input?
> > How do you define non-alpha characters?
> > Will something like *root*child*root* work as well?
> > What if I don't have an array in my language?
>
> Um, do you understand that I was proposing a solution that
> meets your 'specs'? A lot of these questions are good
> ones. Show me show you will specify the answers as tests.

We are discussing tests as specs, not implementations.

You wrote the following:
"Do you really think it would be easier to understand what is required of a program if all you were given were a set of tests to run?"

I thought you were proposing a spec that would make it easier to understand what is required of a program than my
tests.

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Programming with "Duh" Typing Posted: Aug 2, 2007 10:17 AM
Reply to this message Reply
> > Obviously static typing has its place in the industry,
> > simply because some people feel safer with it.
>
> Did you read the article I posted above? It's about
> proving software to be correct statically.

I don't want to get in the flamewar. For me, proving correctness means to mathematically prove that a piece of software does what it should do. The static type systems of C/C++/Java/C# do not allow for proving that.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: word games Posted: Aug 2, 2007 10:18 AM
Reply to this message Reply
> We are discussing tests as specs, not implementations.

Yes. That's true.

> You wrote the following:
> "Do you really think it would be easier to understand what
> is required of a program if all you were given were a set
> of tests to run?"
>
> I thought you were proposing a spec that would make it
> easier to understand what is required of a program than my
> tests.

Yes it was a misunderstanding. I should have made myself more clear. It was a demonstration that your spec doesn't tell me what the software should do. The solution I proposed is not a SAX parser but it would pass your tests. I know what SAX parser should do, but your test doesn't tell me that.

The point is that your tests can never be the sole specification of a program unless your program is trivial. There is no chance that you could provide a set of tests that will verify that the SAX parser meets the requirements of a SAX parser. You'd have to test every possible valid XML document.

Providing a program spec solely in terms of tests is similar to me providing a list of numbers and asking you to write a algebraic function that would produce the same list and more but vastly more complex. This is not easier than just telling someone what you need.

Providing tests is not a bad thing. I think it's great. But specifying requirements only as tests is not feasible for non-trivial applications.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Programming with "Duh" Typing Posted: Aug 2, 2007 10:32 AM
Reply to this message Reply
> > > Obviously static typing has its place in the
> industry,
> > > simply because some people feel safer with it.
> >
> > Did you read the article I posted above? It's about
> > proving software to be correct statically.
>
> I don't want to get in the flamewar.

The flamewar between myself and Isaac is not about anything meaningful.

I disagree with you on this issue but I agree with you on others and I respect your position. Can'twe discuss it rationally? I think your stance is very valid, I just don't think it's as cut-and-dried as you seem to believe it is.

> For me, proving
> correctness means to mathematically prove that a piece of
> software does what it should do. The static type systems
> of C/C++/Java/C# do not allow for proving that.

So your understanding of 'correctness' is at least roughly compatible with mine.

Why must theorem proving be the only way? From the article: "Like theorem proving-based approaches, FSV can be used to verify that all possible executions of a system are consistent with a behavioral specification."

Why do you arbitrarily require that theorem proving be the only way to prove correctness? What reasons do you have to reject FSV?

Please note that I do think that FSV can be used to verify all useful applications. I don't think that we will ever be able to do away with testing.

Petrik de Heus

Posts: 19
Nickname: p8
Registered: Jul, 2007

Re: word games Posted: Aug 2, 2007 3:50 PM
Reply to this message Reply
> > We are discussing tests as specs, not implementations.
>
> Yes. That's true.
>
> > You wrote the following:
> > "Do you really think it would be easier to understand
> what
> > is required of a program if all you were given were a
> set
> > of tests to run?"
> >
> > I thought you were proposing a spec that would make it
> > easier to understand what is required of a program than
> my
> > tests.
>
> Yes it was a misunderstanding. I should have made myself
> more clear. It was a demonstration that your spec doesn't
> tell me what the software should do. The solution I
> proposed is not a SAX parser but it would pass your tests.
> I know what SAX parser should do, but your test doesn't
> t tell me that.
>
Apparently there is no spec for SAX:

"There is no formal specification for SAX. The Java implementation of SAX is considered to be normative, and implementations in other languages attempt to follow the rules laid down in that implementation, adjusting for the differences in language where necessary."
http://en.wikipedia.org/wiki/Simple_API_for_XML

If the Java implementation has a good test set it would be trvial to write a good SAX parser if you had the source as well.

> The point is that your tests can never be the sole
> specification of a program unless your program is trivial.
> There is no chance that you could provide a set of tests
> s that will verify that the SAX parser meets the
> requirements of a SAX parser. You'd have to test every
> possible valid XML document.
>

But a requirement that states that every possible valid XML document should be parsed correctly cannot be verified either and should be rewritten:

"Certain requirements, by their very structure, are not testable. These include requirements that say the system shall never or always exhibit a particular property. Proper testing of these requirements would require an infinite testing cycle. Such requirements are often rewritten to state a more practical time period."
http://en.wikipedia.org/wiki/Requirement

You can of course test corner cases, like minimal number of child_elements or minimal file length. Or use fuzz testing.

> Providing a program spec solely in terms of tests is
> similar to me providing a list of numbers and asking you
> to write a algebraic function that would produce the same
> list and more but vastly more complex. This is not easier
> than just telling someone what you need.

If you tell me to produce the same list that's what I can do.
If you want me to use a special algorithm or a function that's build in, you need to verify it with a test.

> Providing tests is not a bad thing. I think it's great.
> But specifying requirements only as tests is not feasible
> e for non-trivial applications.

I wouldn't call JRuby trivial.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: word games Posted: Aug 2, 2007 4:00 PM
Reply to this message Reply
James Watson wrote
> > That's right - a change to the specification requires a
> > change to the tests which may require a change to the
> > formerly correct program before it could be considered
> > correct once more, what's surprising about that?
>
> I didn't say anything about a change to the specification.

If the spec didn't change then what do you mean "a correct program could be become incorrect without changing anything about it"?

> The above is only true in the case where the tests are
> e the specification. That is not how specifications are
> normally documented.

How are implementations normally checked against specs? (I think acceptance tests are far more common than formal proof.)


> > Verification checks conformance to spec - correctness.
> >
> > Validation checks what was really wanted - "meets all
> > requirements".
>
> And I'm the one playing word games. Unbelievable.

Perhaps you aren't familiar with that simple distinction, perhaps you haven't come across those technical terms but they are well established terms (IEEE 729 "Glossary of Software Engineering Terminology" 1982) and commonly used.

The authors of a 2002 IBM SYSTEMS JOURNAL article wanted to be "accessible to the students of software engineering at large" so they included some definitions for "relevant terminology":

Thus, verification is the process of proving or demonstrating that the program correctly satisfies the specifications. Notice that we use the term verification in the sense of “functional correctness”...

Validation is the process of evaluating software, at the end of the development process, to ensure compliance with requirements.



> You are trying to side step the issue. It's very
> possible, common even, to have a program that passes all
> tests that doesn't meet all requirements. Do you consider
> such a program to be correct?

There isn't an issue for me to side step.

It's no more than a matter of definition, so what matters is that a definition is provided and agreed.

Just Google correct or correctness and you'll find a wikipedia article that might be helpful - http://en.wikipedia.org/wiki/Correctness

When we use tests to check the program conforms to spec, and the program passes all tests, and we're using an ordinary definition of program correctness, then the program is obviously 'correct'.

If we were using the definition that you have come up with then the program is obviously not 'correct'.

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Re: word games Posted: Aug 2, 2007 4:04 PM
Reply to this message Reply
>> Providing tests is not a bad thing. I think it's great.
>> But specifying requirements only as tests is not feasible
>> e for non-trivial applications.
>
>I wouldn't call JRuby trivial.

Isn't JRuby mostly specified by Matz's version of Ruby?

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Verification and Validation Posted: Aug 2, 2007 4:17 PM
Reply to this message Reply
http://www.research.ibm.com/journal/sj/411/hailpern.html

Verification: Given a program and a set of specifications, show that the program satisfies those specifications (given P and a set of specifications = {1, 2, 3, … , n}, show that P satisfies ). Thus, verification is the process of proving or demonstrating that the program correctly satisfies the specifications.2 Notice that we use the term verification in the sense of “functional correctness,” which is different from the typical discussion of verification activities discussed in some software engineering literature,3,4 where it applies to ensuring that “each step of the development process correctly echoes the intentions of the immediately preceding step.”

Note that the article admits that its definition is inconsistent with what is used in "some" software engineering literature.


Validation: Validation is the process of evaluating software, at the end of the development process, to ensure compliance with requirements. Note that the verification community also uses the term validation to differentiate formal functional verification from extensive testing of a program against its specifications.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: Verification and Validation Posted: Aug 2, 2007 4:38 PM
Reply to this message Reply
Erik Engbrecht wrote
> Note that the article admits that its definition is
> inconsistent with what is used in "some" software
> engineering literature.

Which is less interesting than it might seem, IEEE 729 gave three definitions for verification :-)

- determining whether or not the products of a given phase fulfil the requirements established during the previous phase

- formal proof of program correctness

- establishing whether or not stuff conforms to specified requirements

And one definition for validation:

- evaluating software at the end of development to ensure compliance with software requirements

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: word games Posted: Aug 2, 2007 5:51 PM
Reply to this message Reply
> But a requirement that states that every possible valid
> XML document should be parsed correctly cannot be verified
> either and should be rewritten:

So you propose reducing what can be done with software to only simple things that can be completely verified with tests? I think you'll have hard time selling that to almost anyone.

> "Certain requirements, by their very structure, are not
> testable. These include requirements that say the system
> shall never or always exhibit a particular property.
> Proper testing of these requirements would require an
> infinite testing cycle. Such requirements are often
> rewritten to state a more practical time period."
> http://en.wikipedia.org/wiki/Requirement

I agree that many requirements are not testable. Rewriting them to be something different does not change that.

> You can of course test corner cases, like minimal number
> of child_elements or minimal file length. Or use fuzz
> testing.

Everyone in this discussion knows these things.

> > Providing a program spec solely in terms of tests is
> > similar to me providing a list of numbers and asking
> you
> > to write a algebraic function that would produce the
> same
> > list and more but vastly more complex. This is not
> easier
> > than just telling someone what you need.
>
> If you tell me to produce the same list that's what I can
> do.
> If you want me to use a special algorithm or a function
> that's build in, you need to verify it with a test.

Sorry, not following your logic.

> > Providing tests is not a bad thing. I think it's
> great.
> > But specifying requirements only as tests is not
> feasible
> > e for non-trivial applications.
>
> I wouldn't call JRuby trivial.

I wouldn't say JRuby is defined by tests. From what I understand, Ruby doesn't have a formal specification or at least it didn't in the past.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: word games Posted: Aug 2, 2007 6:12 PM
Reply to this message Reply
> James Watson wrote
> > > That's right - a change to the specification requires
> a
> > > change to the tests which may require a change to the
> > > formerly correct program before it could be
> considered
> > > correct once more, what's surprising about that?
> >
> > I didn't say anything about a change to the
> specification.
>
> If the spec didn't change then what do you mean "a correct
> program could be become incorrect without changing
> anything about it"?

I you define correctness as passing all tests, creating a new test that exposed an existing issue (with regard to specifications) would make the code incorrect.

> > The above is only true in the case where the tests are
> > e the specification. That is not how specifications
> are
> > normally documented.
>
> How are implementations normally checked against
> specs? (I think acceptance tests are far more common than
> formal proof.)

Testing.

> > > Verification checks conformance to spec -
> correctness.
> > >
> > > Validation checks what was really wanted - "meets all
> > > requirements".
> >
> > And I'm the one playing word games. Unbelievable.
>
> Perhaps you aren't familiar with that simple distinction,
> perhaps you haven't come across those technical terms but
> they are well established terms (IEEE 729 "Glossary of
> Software Engineering Terminology" 1982) and commonly used.
>
>
> The authors of a 2002 IBM SYSTEMS JOURNAL article wanted
> to be "accessible to the students of software engineering
> at large" so they included some definitions for "relevant
> terminology":
>
> Thus, verification is the process of proving or
> demonstrating that the program correctly satisfies the
> specifications. Notice that we use the term verification
> in the sense of “functional correctness”...

>
> Validation is the process of evaluating software, at
> the end of the development process, to ensure compliance
> with requirements.


How is this incompatible with what I am arguing?

> > You are trying to side step the issue. It's very
> > possible, common even, to have a program that passes
> all
> > tests that doesn't meet all requirements. Do you
> consider
> > such a program to be correct?
>
> There isn't an issue for me to side step.
>
> It's no more than a matter of definition, so what matters
> is that a definition is provided and agreed.
>
> Just Google correct or correctness and
> you'll find a wikipedia article that might be helpful -
> http://en.wikipedia.org/wiki/Correctness

I don't see where this is contradicting me in any way. Perhaps you should try to understand my point before arguing about it.

> When we use tests to check the program conforms to spec,
> and the program passes all tests, and we're using an
> ordinary definition of program correctness, then the
> program is obviously 'correct'.

If all tests pass, it doesn't mean that the spec is completely satisfied unless the spec is defined by the tests.

> If we were using the definition that you have come up with
> then the program is obviously not 'correct'.

In any other case other than that of which the spec is completely defined by tests all testing can do is prove that a program is incorrect for non-trivial programs. It cannot prove the program correct unless it tests all possible states of the application.

In practical terms, it's possible to test a program and have a good confidence in it's correctness. But you can never prove a program to be correct in the terms that Achilleas Margaritis describes as "proving correctness means to mathematically prove that a piece of software does what it should do." And this the commonly understood defintion between myself and Achilleas when you decided to start an argument about what correct means.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Verification and Validation Posted: Aug 2, 2007 6:14 PM
Reply to this message Reply
> Erik Engbrecht wrote
> > Note that the article admits that its definition is
> > inconsistent with what is used in "some" software
> > engineering literature.
>
> Which is less interesting than it might seem, IEEE 729
> gave three definitions for verification :-)
>
> - determining whether or not the products of a given phase
> fulfil the requirements established during the previous
> phase

Testing doesn't do this.

> - formal proof of program correctness

Testing doesn't do this.

> - establishing whether or not stuff conforms to specified
> requirements

Testing doesn't do this.

> And one definition for validation:
>
> - evaluating software at the end of development to ensure
> compliance with software requirements

Testing doesn't do this.

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Programming with "Duh" Typing Posted: Aug 3, 2007 1:42 AM
Reply to this message Reply
> Why do you arbitrarily require that theorem proving be the
> only way to prove correctness? What reasons do you have
> to reject FSV?
>

I am not a specialist or a mathematician, but I hang out long enough in LtU to learn to appreciate theorem proving. I would like my software not to have any corner cases that bugs might lurk in. Of course that's not entirely doable with current technology...

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Programming with "Duh" Typing Posted: Aug 3, 2007 6:17 AM
Reply to this message Reply
> > Why do you arbitrarily require that theorem proving be
> the
> > only way to prove correctness? What reasons do you
> have
> > to reject FSV?
> >
>
> I am not a specialist or a mathematician, but I hang out
> long enough in LtU to learn to appreciate theorem proving.
> I would like my software not to have any corner cases that
> bugs might lurk in. Of course that's not entirely doable
> with current technology...

Complete FSV proves all possible states are consistent with the specification. It is doable with currrent technology (as the article explains) but not for all applications. Probably very few at this point.

In any event, what I don't understand about your argument is that testing doesn't prove software correct (e.g. theorem proving) either. If you are going to reject static typing for this reason you should also reject testing. Clearly that's absurd so I would like to discuss the real reasons why you think static typing should not be used.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: word games Posted: Aug 3, 2007 10:31 AM
Reply to this message Reply
James Watson wrote
> I you define correctness as passing all tests, creating a
> new test that exposed an existing issue (with regard to
> specifications) would make the code incorrect.

And why would we create a new test?


> > How are implementations normally checked against
> > specs? ...
>
> Testing.

So normally tests represent the specification?


> How is this incompatible with what I am arguing?

The only way we can validate a program 'meets all requirements' is to ask someone "is this what you wanted?".

We can verify that a program is 'correct' by demonstrating that it satisfies the spec.


> > When we use tests to check the program conforms to
> > spec, and the program passes all tests, and we're using
> > an ordinary definition of program correctness, then the
> > program is obviously 'correct'.
>
> If all tests pass, it doesn't mean that the spec is
> completely satisfied unless the spec is defined by the
> tests.

It isn't true unless it's true! What a tortuous way to avoiding saying - if the spec is defined by tests and all the tests pass then the spec is completely satisfied.


> In practical terms, it's possible to test a program and
> have a good confidence in it's correctness. But you can
> never prove a program to be correct in the terms that
> Achilleas Margaritis describes as "proving correctness
> means to mathematically prove that a piece of software
> does what it should do." And this the commonly understood
> defintion between myself and Achilleas when you decided to
> start an argument about what correct means.

You can never mathematically prove a program to be correct when your idea of 'correct' is 'meets all requirements' - it's a category error - 'meets all requirements' is outside the formal domain of mathematics.

Flat View: This topic has 370 replies on 25 pages [ « | 21  22  23  24  25 | » ]
Topic: Programming with "Duh" Typing Previous Topic   Next Topic Topic: Python 3000 Plea for Help

Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2019 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use