Home > Archive > Extreme Programming > January 2005 > Testing for things statically checked at build-time.
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
Testing for things statically checked at build-time.
|
|
| Steve Jorgensen 2005-01-17, 8:56 am |
| I was just doing some thinking about DbC with static checking, and realized
that some cases where one would normally write a test to assert failure cannot
be written because they have to break the contract to run, and therefore will
not build.
Thinking a bit more, I realized the same type of thing is true of typesafe
languages like Java as well. There are things that one might write a test to
assert failure of in, say, Smalltalk, that one cannot even compile the test
for in Java because it fails by violating type safety.
Now, here's why I'm thinking this is an issue regardless whether you advocate
for or against type safety or statically checked contracts in general. How do
you write a repeatable test for the invalidity of something that demonstrates
its invalidity by failing to build? You can write a one-time test, and see
that the compile does fail in the expected way, but you can't add it to the
test suite, or you can no longer build and run the test suite.
Alright, I know I haven't provided any concrete examples to show that this
issue matters, so consider it a philosophical rather than practical question
for the moment. If I come up with any concrete examples in the next few days,
I'll post back with that.
| |
| Ron Jeffries 2005-01-17, 8:56 am |
| On Mon, 17 Jan 2005 00:25:36 -0800, Steve Jorgensen
<nospam@nospam.nospam> wrote:
>Now, here's why I'm thinking this is an issue regardless whether you advocate
>for or against type safety or statically checked contracts in general. How do
>you write a repeatable test for the invalidity of something that demonstrates
>its invalidity by failing to build? You can write a one-time test, and see
>that the compile does fail in the expected way, but you can't add it to the
>test suite, or you can no longer build and run the test suite.
It feels to me as if there's no point to writing a test for an error
that won't even compile. So I wouldn't want to write it. I look
forward to an example.
>
>Alright, I know I haven't provided any concrete examples to show that this
>issue matters, so consider it a philosophical rather than practical question
>for the moment. If I come up with any concrete examples in the next few days,
>I'll post back with that.
I think that will help.
--
Ron Jeffries
www.XProgramming.com
I'm giving the best advice I have. You get to decide if it's true for you.
| |
| Steve Jorgensen 2005-01-17, 3:57 pm |
| On Mon, 17 Jan 2005 07:02:53 -0500, Ron Jeffries <ronjeffries@acm.org> wrote:
>On Mon, 17 Jan 2005 00:25:36 -0800, Steve Jorgensen
><nospam@nospam.nospam> wrote:
>
>
>It feels to me as if there's no point to writing a test for an error
>that won't even compile. So I wouldn't want to write it. I look
>forward to an example.
Well, staying in philosophical mode for the moment, if the expected behavior
is a failure of certain code to compile, the reason for the test would be to
ensure that such code continues to fail to compile as future changes are made.
>
>I think that will help.
On thinking of how I would create a contrived example, I realize that for a
simple typesafe language like Java, this issue might never exist since a test
could probably just attempt to pass an object in a variable of Object type,
and expect a runtime error. On the other hand, with Extended Static Checking
or Type Inference, such code might actually fail to build because the checker
can see that such code will break the rules.
| |
| jgrigg@mo.net 2005-01-17, 3:57 pm |
| A: Invoke the compiler during the test.
That is, in the test, write a source file to a temporary directory, and
then compile it. Due to strict type checking, in the compiler, the
compile will fail.
Example:
I'm writing
String reverse(String sourceString);
Should someone write this code:
int reversed = reverse(12345); // expecting the value 54321 to be
returned
I want their compile to fail.
So, to test it, I'll invoke the compiler.
But normally, I don't worry about it. I have /some/ trust in the
compiler. ;->
Does this help?
| |
| Dirk Thierbach 2005-01-17, 8:56 pm |
| Steve Jorgensen <nospam@nospam.nospam> wrote:
> I was just doing some thinking about DbC with static checking, and
> realized that some cases where one would normally write a test to
> assert failure cannot be written because they have to break the
> contract to run, and therefore will not build.
> Now, here's why I'm thinking this is an issue regardless whether you
> advocate for or against type safety or statically checked contracts
> in general. How do you write a repeatable test for the invalidity
> of something that demonstrates its invalidity by failing to build?
> You can write a one-time test, and see that the compile does fail in
> the expected way, but you can't add it to the test suite, or you can
> no longer build and run the test suite.
> Alright, I know I haven't provided any concrete examples to show
> that this issue matters, so consider it a philosophical rather than
> practical question for the moment. If I come up with any concrete
> examples in the next few days, I'll post back with that.
I am not sure I understand completely what you want, but maybe the
following very simple example fits. I am using Haskell, because its
typesystem makes things sufficiently easy.
When doing DbC in a statically typed language, one can encode a
precondition in a type. Say we want to write a minimum function
that operates only on lists that are already sorted (because that
makes the function quite simple :-). So the precondition is that
the list is sorted. We define a new type synonym for that:
> newtype SortedList a = SL [a]
Then we can write the minimum function
> sortedMin (SL (x:_)) = x
and type inference will figure out it has the type
> sortedMin :: SortedList a -> a
So the precondition has become part of the type signature. Now we only
have to make sure that all low-level functions which produce sorted
lists return the right type, and then the type checker will guarantee
that this precondition will never be violated (otherwise the
program won't compile).
This differs from the "write an assertion to check the list is sorted"
approach because (a) the compiler will optimize away the type synonym,
so there's no performance penalty and (b) an assertion can only fail
for particular examples, but maybe (by bad luck) all the test cases we
have will only call our minimum function with a sorted lists. So all
the tests will pass, but in reality there might be some border case
which will call our function with an unsorted list, and this will be
only detected when the program is already in use.
Or, to express it differently, if TDD does "specification by example"
and tests for success of a specific test case, here we do "specification
by restriction", and make a "compile-time" test which is encoded in
the type, and checked on *all* (abstract) execution paths of the complete
program before execution.
Is this close to what you wanted? The test is explicit in the type
signature (which may even be inferred by the type checker), and
"repeatable" (if you want) at compile-time.
- Dirk
| |
| Steve Jorgensen 2005-01-18, 3:56 am |
| ....
>Or, to express it differently, if TDD does "specification by example"
>and tests for success of a specific test case, here we do "specification
>by restriction", and make a "compile-time" test which is encoded in
>the type, and checked on *all* (abstract) execution paths of the complete
>program before execution.
I guess what I'm saying is that if it's checked by the compiler, the invalid
case cannot be checked by a test (short of writing code to a file and
compiling it as a testing task). So that means we can't have a test that
verifies that the static check excludes the cases we think it should. Any
such test would fail to build.
| |
| Ron Jeffries 2005-01-18, 3:56 am |
| On Mon, 17 Jan 2005 07:56:45 -0800, Steve Jorgensen
<nospam@nospam.nospam> wrote:
>Well, staying in philosophical mode for the moment, if the expected behavior
>is a failure of certain code to compile, the reason for the test would be to
>ensure that such code continues to fail to compile as future changes are made.
I wouldn't test that, either. Nor would I test whether a + b still
compiles. I test things that I think are likely to break.
>
>
>On thinking of how I would create a contrived example, I realize that for a
>simple typesafe language like Java, this issue might never exist since a test
>could probably just attempt to pass an object in a variable of Object type,
>and expect a runtime error. On the other hand, with Extended Static Checking
>or Type Inference, such code might actually fail to build because the checker
>can see that such code will break the rules.
Rite.
--
Ron Jeffries
www.XProgramming.com
I'm giving the best advice I have. You get to decide if it's true for you.
| |
| Dirk Thierbach 2005-01-18, 8:59 pm |
| Steve Jorgensen <nospam@nospam.nospam> wrote:
> ...
[color=darkred]
> I guess what I'm saying is that if it's checked by the compiler, the
> invalid case cannot be checked by a test (short of writing code to a
> file and compiling it as a testing task).
> So that means we can't have a test that verifies that the static
> check excludes the cases we think it should. Any such test would
> fail to build.
Yes, but why is that bad? The approach TDD uses works because you're
writing "positive" tests: Things that should happen. You write the
test (the specification) first, it fails, then you change the code,
and it passes. You don't write tests for the invalid case; it remains
unspecified. (Unless you're testing your error routines. In that
case, you have again turned it into a "positive" thing: The "result"
should be an "error value").
You can use a similar approach for static checking: Write the type
signature (the specification) first. Compilation fails unless
you get the code right, and then it "passes".
(Or, you can be lazy, and use type inference to get the signature,
and compare it to the signature you'd expect).
Since the specification expresses a property of the code, I don't
see where an "invalid case" should come from. An invalid case would
be wrong code, but no one is interested in that.
What you cannot test completely is that the abstract name for the
property really expresses the property that you want. Again, you only
can test "positively" with assertions that for some example cases, the
values for a restricted type are correct. You cannot test the
"negative" case (that no invalid values will ever appear in that
restricted type) explicitely, but you can do a formal proof on the
limited number of constructors for that type. (Or you can do a less
"formal" proof by code inspection and convincing yourself that it
works).
But that's not a drawback, since for dynamic tests, there's no way at
all you can be sure your examples are exhaustive, and really cover all
relevant cases. With static checks, there's at least the possibility
to prove it as outlined above (after all, that's why you can use
static checks for the "negative" case at all, where "positive" examples
will never suffice).
Im I making any sense? Or am I still missing the point?
- Dirk
| |
| Steve Jorgensen 2005-01-19, 8:58 am |
| On Tue, 18 Jan 2005 09:39:55 +0100, Dirk Thierbach <dthierbach@gmx.de> wrote:
>Steve Jorgensen <nospam@nospam.nospam> wrote:
>
>
>
>Yes, but why is that bad? The approach TDD uses works because you're
>writing "positive" tests: Things that should happen. You write the
>test (the specification) first, it fails, then you change the code,
>and it passes. You don't write tests for the invalid case; it remains
>unspecified. (Unless you're testing your error routines. In that
>case, you have again turned it into a "positive" thing: The "result"
>should be an "error value").
>
>You can use a similar approach for static checking: Write the type
>signature (the specification) first. Compilation fails unless
>you get the code right, and then it "passes".
>
>(Or, you can be lazy, and use type inference to get the signature,
>and compare it to the signature you'd expect).
>
>Since the specification expresses a property of the code, I don't
>see where an "invalid case" should come from. An invalid case would
>be wrong code, but no one is interested in that.
Well, my reasoning is that the tests should specify the code behavior, and
it's good that they are located outside the code. With contracts written
inside the code, what if you have to make a contract more complex to be less
restrictive? Are you still confident that the contract specifies what you
think it does?
>What you cannot test completely is that the abstract name for the
>property really expresses the property that you want. Again, you only
>can test "positively" with assertions that for some example cases, the
>values for a restricted type are correct. You cannot test the
>"negative" case (that no invalid values will ever appear in that
>restricted type) explicitely, but you can do a formal proof on the
>limited number of constructors for that type. (Or you can do a less
>"formal" proof by code inspection and convincing yourself that it
>works).
All well and good, but that fails to provide one big thing the tests are for,
that is to retain confidence in your code as refactoring is done. After you
refactor, you can hit a button and re-run your tests. Can you hit a button
and re-run your code-inspection proof?
>But that's not a drawback, since for dynamic tests, there's no way at
>all you can be sure your examples are exhaustive, and really cover all
>relevant cases. With static checks, there's at least the possibility
>to prove it as outlined above (after all, that's why you can use
>static checks for the "negative" case at all, where "positive" examples
>will never suffice).
Of course, static analysis has benefits tests do not, or I wouldn't even care
enough to discuss it. It looks to me, though, like static analysis also does
not do some things tests do, and at the same time, it seems to make some of
those tests impossible or very difficult to do while also hiding a valid case
for doing those tests.
>
>Im I making any sense? Or am I still missing the point?
Yes, you are making sense. I still feel the issue is not resolved, though.
At the same time, I do acknowledge that I may be making a mountain out of a
mole hill. I hope, at some point to do enough TDD in conjunction with Static
Analysis to try to measure whether issue has any demonstrable real-world
impact.
| |
| Dirk Thierbach 2005-01-19, 8:58 am |
| Steve Jorgensen <nospam@nospam.nospam> wrote:
[color=darkred]
> Well, my reasoning is that the tests should specify the code behavior, and
> it's good that they are located outside the code.
Yes.
> With contracts written inside the code,
I am not sure I'd say a type signature "contract" is written inside
the code. Type signatures are optional (for sensible type systems
which support type inference). I keep them usually close to the
function, yes, but that's mainly for convenience. In Haskell, e.g.,
the only restriction is that they are in the same module, so
no one keeps you from collecting all type signatures in one place,
if you wanted to.
> what if you have to make a contract more complex to be less
> restrictive?
That's difficult to do with an abstract name for a concrete
property of some type. You'll have to inspect all "basic" functions
that use this type. So ...
> Are you still confident that the contract specifies what you think
> it does?
.... to make sure nothing goes wrong, I'd change the abstract name,
and then let the compiler walk me through all functions that are
affected (because compilation will fail for those functions).
I'd inspect them and change them so they work again.
For example, the minimum function only works when the list is
non-empty. So if I wanted to strengthen the precondition to "non-empty
sorted list", I'd change the declaration to
> newtype SortedNonemptyList a = SNEL [a]
This will make alll the static tests fail, so I can go through
them and make sure in each case I really get a non-empty list.
(In reality, I'd do a large part of that with search-and-replace
before I'd attempt the recompilation, and let then the compiler
just point out those places I have overlooked).
[color=darkred]
> All well and good, but that fails to provide one big thing the tests
> are for, that is to retain confidence in your code as refactoring is
> done. After you refactor, you can hit a button and re-run your
> tests. Can you hit a button and re-run your code-inspection proof?
Yes, but not with a button hit. The code-inspection proof is
"incremental": For each basic function which returns a value of that
type, I have to check that under the assumption the property in
questions holds for all input values, it will also hold for the output
value. If I refactor such a function, I have to inspect the new
functions in this respect. I don't have to inspect the unchanged
functions, because I already did that some time ago, and the
refactoring won't affect them (refactoring doesn't change semantics).
And the compiler will assist me in pointing out any location where the
new type might have "crept in" during refactoring, even if I didn't
realize it.
> Of course, static analysis has benefits tests do not, or I wouldn't
> even care enough to discuss it. It looks to me, though, like static
> analysis also does not do some things tests do, and at the same
> time, it seems to make some of those tests impossible or very
> difficult to do while also hiding a valid case for doing those
> tests.
Maybe that's the point I don't understand. Static analysis and
tests by example are complementary in some sense. Static analysis
allows you to test "negative" properties on all execution paths,
tests by example allows you to test "positive" properties on one
specific execution path. In this respect, none of them does what
the other allows to do.
So I don't see why any of them should hides a "valid test case",
besides their in-built deficiencies (as discussed before). I don't
expect test by example to let me automatically verify that I didn't
miss any important test case. Neither do I expect static analysis to
let me automatically verify that the property I want to encode is
really the one I wanted (with a very good automatic theorem proving
system I could to some degree, but there is no such system that is
sufficiently powerful to be practical for the working programmer at
the moment).
[color=darkred]
> Yes, you are making sense. I still feel the issue is not resolved,
> though.
Then I am probably still missing something.
> At the same time, I do acknowledge that I may be making a mountain
> out of a mole hill.
Or maybe you're missing some kind of "aha, that's the right way
to look at it" effect :-)
- Dirk
|
|
|
|
|