In fact unit testing and formal methods could reinforce each other, but IMO the tools for this approach are missing.
Say the system you want to test has an "input space" (all combinations of possible input parameters) and some output ( a program that doesn't do anything , produce something or has a side effect, is useless). Unit testing is all about defining a series of a "test cases". In each test case we
set up a precondition;
deliver an input for the function to perform;
then do some checks on the result.
Writing a new test case is only usefull when it verifies another "behaviour" of the system. Take a look at the way XP approaches testing:
write some tests
then write the code that implements the tests
then try to "break" the system by writing a test that makes the system fail
then enhance the code to work with the new test
retest with all tests to verify regression
repeat.
If you look at this procedure in a more abstract way you could say that intuitively you are "partitioning" the input space of the method, where in each partition the system has a different behaviour, described by the representative testcase. So a test case is a representative of a whole class of uses of the system where the system has similar behaviour.
A word on my experience with formal methods : When I started writing unit tests, I noticed some similarities with notions of formal methods I encountered at university:
Hoare calculus also has this structure of pre- and postconditions. Formal verification of programs using Hoare calculus is a bottom-up process: first one specifies a formal proof of a trivial step of a program (e.g. 1 assignment) by describing the state of the program before and after execution of the trivial step (aka describing the pre- and post condition). The verification of such a trivial step consists by simply stating one of the axioms of the calculus. The calculus then provides compositional rules to combine trivial steps in more and more complex algorithms, and in the process the pre- and postconditions of the composed statements are combined in more complex pre- and post conditions for the whole algorithm.
A similar approach is "stepwise refinement" or "transformation". In this case a method is first entirely formally described, but without an explicit algorithm. The formal description is then step by step transformed into an executable algorithm. Each step is "verifiable", i.e. preserves ths semantics of the formal specification.
"Abstract datatypes" (ADT's) and "rewrite systems" have notions of "sufficient amount of specification". An ADT is some sort of "mathematical class", where the methods on the class are formally specified by specifying logical statements about relationships between methods.(e.g an ADT "stack" could have methods "push", "pop", "isempty", and a specification "performing a pop after a push on an empty stack returns an empty stack", which is then writtten formally in some logical language like pop(push(isempty())) == isempty(), etc... )
Once one has sated enough relationships between an ADT's methods, it is fully specified. What is interesting is that there are formal methods to tell
whether an abstract datatype is "underspecified", so the ADT needs more statements to be fully specified
to verify whether a problem is "overspecified".
The similarities are only vague: hoare calculus verifies a method, but the partitioning is oriented on the program structure, not on the input cases. ADT's do not specify a single method, but a whole class, but the similarity is that there is a process of "finding the right amount of specification".
Both formal and unit testing have their own strenghts and weaknesses:
Formal verification
tends to be very elaborate. a typical comment you hear about formal testing is that it "is only justified for systems where every failure is critical and unacce
but wouldn't it be nice to try and keep the java language *simple*?
isn't syntactic sugaring all about making code more readable? I think boxing , generics, typesafe enums, static imports make the java language more simple to use.
It's just looking over the fence to the "sibling" languages (c++, c#) and copy what they do better.
In one of Terry Pratchett's books -can't remember which one- there is a guy with an absolute memory. When asked for his earliest memory, he says : there was a big light and somebody hit me.
taking a certification when you have already years of experience is a waste of time. It's when you start in a field that you should aim at a certification asap. If you just learn something on the job, you risk to have experience with only a subset of the field, projects rarely address everything a language/platform/OS... has to offer. Courses offer a wider range, but when you go for a certification, you are forced to go into the depth of things and really master them.
The point is: learning towards an exam gives the best learning curve. It sets clear objectives, keeps you focused and lets you advance at a better pace. While studying, do an exam simulation from time to time, it can be a good objective progress indicator. When you're ready, take the exam: then you cannot fool yourself, and see if you're "ready for production".
Of course all this requires that the exam is of good quality. I am not MS oriented, so cannot speak of MCSE (but I can imagine:-) ) but IMO, e.g. the SUN and IBM exams worked very well for this purpose.
Slashdot Mirror
Say the system you want to test has an "input space" (all combinations of possible input parameters) and some output ( a program that doesn't do anything , produce something or has a side effect, is useless). Unit testing is all about defining a series of a "test cases". In each test case we
Writing a new test case is only usefull when it verifies another "behaviour" of the system. Take a look at the way XP approaches testing:
If you look at this procedure in a more abstract way you could say that intuitively you are "partitioning" the input space of the method, where in each partition the system has a different behaviour, described by the representative testcase. So a test case is a representative of a whole class of uses of the system where the system has similar behaviour.
A word on my experience with formal methods : When I started writing unit tests, I noticed some similarities with notions of formal methods I encountered at university:
A similar approach is "stepwise refinement" or "transformation". In this case a method is first entirely formally described, but without an explicit algorithm. The formal description is then step by step transformed into an executable algorithm. Each step is "verifiable", i.e. preserves ths semantics of the formal specification.
The similarities are only vague: hoare calculus verifies a method, but the partitioning is oriented on the program structure, not on the input cases. ADT's do not specify a single method, but a whole class, but the similarity is that there is a process of "finding the right amount of specification".
Both formal and unit testing have their own strenghts and weaknesses:
Formal verification
"My flexible friend" (putting butter on his sandwich using his creditcard)
isn't syntactic sugaring all about making code more readable? I think boxing , generics, typesafe enums, static imports make the java language more simple to use.
It's just looking over the fence to the "sibling" languages (c++, c#) and copy what they do better.
The Empire.
In one of Terry Pratchett's books -can't remember which one- there is a guy with an absolute memory. When asked for his earliest memory, he says : there was a big light and somebody hit me.
"I am sure I put it somewhere over here." CLUNK! "Ohw!"
taking a certification when you have already years of experience is a waste of time. It's when you start in a field that you should aim at a certification asap. If you just learn something on the job, you risk to have experience with only a subset of the field, projects rarely address everything a language/platform/OS... has to offer. Courses offer a wider range, but when you go for a certification, you are forced to go into the depth of things and really master them. The point is: learning towards an exam gives the best learning curve. It sets clear objectives, keeps you focused and lets you advance at a better pace. While studying, do an exam simulation from time to time, it can be a good objective progress indicator. When you're ready, take the exam: then you cannot fool yourself, and see if you're "ready for production". Of course all this requires that the exam is of good quality. I am not MS oriented, so cannot speak of MCSE (but I can imagine :-) ) but IMO, e.g. the SUN and IBM exams worked very well for this purpose.