Domain: ucd.ie
Stories and comments across the archive that link to ucd.ie.
Comments · 45
-
Re:Because old machines are perfectly fine!
I agree. This is me playing the new Tomb Raider: http://mathsci.ucd.ie/~plynch/eniac/ENIAC.jpg
It's slow as shit
:( -
Re:Let me get this straight
Exactly. There are many psychological variations between populations from different cultures as this article points out.
-
Re:DEC did a good one
One of the best ones was the DEC Extended Static Checker for Java in the late 1990s. That project died after Compaq acquired DEC and shut down research. But it formed part of Microsoft's efforts for Spec#, which has a formal verification system.
ESC/Java lives on as ESC/Java2 which uses the JML language for annotation. This makes it significantlymore powerful than ESC/Java since you also get the entire JML toolchain as well. ESC/Java2 also has excellent IDE support via Eclipse plugins now. If you like that sort of thing it is well worth looking into.
-
Re:DWDM
...it's disappointing to find out that he is not an ex-UC Davis alumnus as the summary implies
The summary speaks of "of a group of ex-UCD photonics researchers"; there's more than one UCD on the planet, and this one is probably University College Dublin.
The founders were from UCD, according to the "about Intune" page. ("Intune was founded in 1999 by two college graduates, John Dunne and Tom Farrell. They were performing research on tunable lasers and their network applications in University College Dublin, Ireland.")
(I hope, for UCD's sake, that their Web designers aren't ex-UCD. Not only do they appear to think that "company" is spelled "copmany", the site is a Flash-infested mess that requires you to pop up several layers of menus, by clicking on little + signs, for each member of the management team whose biography you want to see.)
-
Re:Useless
Java is also the perfect high security language, because you can't make security holes with it. Same with C#. Same with VB.NET. We've heard this again and again from people who simply don't understand the problem.
Yes, the first assumption should always be that the NSA don't understand security... Or perhaps there are languages and tools that help you write more secure code. Let's be honest, the average Java program is more secure than the average C program, thanks to slightly stronger type checking and bounds checking. Sure, Java isn't a going to magically make your code perfectly secure, but it does make it a little harder to make mistakes, and a little easier to catch them when you do make them. One can imagine that perhaps there are other things that can be done to make mistakes harder again to make, and even easier to catch. Sure, it's all incremental, and nothing is going to be a silver bullet, but enough small gains and it can become worthwhile for software you want to be robust and/or secure.
I've programmed in C and Java, and I've also played with SPARK Ada. Believe me when I tell you that SPARK really does make a huge difference in catching mistakes. Just using SPARK won't magically make your code secure, but it will provide you with very powerful tools to help you write secure code. It really is a very distinct improvement. If it's the Ada part that you find distasteful, then check out JML and ESC/Java2 which provide similar (though not quite as powerful) facilities for Java.
-
Re:No, just very, very difficult to do right.
You consider obtaining the data content and algorithms by physically dismantling the chip, but I think the whole point of PUFs is that the physical structure of the chip is part of its data content, and thus would also have to be recorded in a reproducible fashion in order to clone.
There was a talk on this at last year's Elliptic Curve Crypto workshop by Pim Tuyls of Philips, but the slides aren't available online (the problem of working in industry instead of academia I guess- everyone elses are available). Doesn't take long to google up papers on the theoretical basis, but I can't rememeber how far along they were at the hardware level unfortunately.
-
Re:Source code is its own documentationIt also makes finding errors easier, as your code may not be doing what your specifications say it should do. In this day and age, if the code has some (suitably formatted) comments regarding what it is supposed to do, you can even get some pretty useful tools to automatically check the code against the specification. It's not bullet-proof, but it can catch a lot of subtle bugs that might get overlooked, particularly in subtely incorrect {use of|calls to} code that you didn't necessarily write yourself. See ESC/Java2 or Spec# to see what I mean.
-
Re:Of course they can workSuch tools work in a very similar way to what is already being done in many modern language compilers (such as javac). Basically, they implement semantic checks that verify whether the program makes sense, or is likely to work as intended in some respect. The keywords here, for the purposes of good static analysis tools, are "work as intended". Knowing what code is intended to do isn't trivial, and it can be severely limiting in what static analysis tools can check for (or, alternatively, they can spit back a lot of false positives). A good solution is provide the static analysis tool with some hints as to what the programmers intentions are -- that means annotations as used by splint, or ESC/Java2, or something similar. The benefits for static analysis (and API documentation depending on the tools) can far outweigh the "extra" work*; consider the sorts of errors ESC/Java2 can successfully catch for instance. Of course you have to be interested in doing static anaylsis to begin with, btu the benefits are definitely available.
* Note that "extra" is in scare quotes because ultimately most of the annotations are usually things you should be documenting anyway, so it's not so much "extra" work as documentation that gets done sooner rather than later. -
Re:Of course they can workSuch tools work in a very similar way to what is already being done in many modern language compilers (such as javac). Basically, they implement semantic checks that verify whether the program makes sense, or is likely to work as intended in some respect. The keywords here, for the purposes of good static analysis tools, are "work as intended". Knowing what code is intended to do isn't trivial, and it can be severely limiting in what static analysis tools can check for (or, alternatively, they can spit back a lot of false positives). A good solution is provide the static analysis tool with some hints as to what the programmers intentions are -- that means annotations as used by splint, or ESC/Java2, or something similar. The benefits for static analysis (and API documentation depending on the tools) can far outweigh the "extra" work*; consider the sorts of errors ESC/Java2 can successfully catch for instance. Of course you have to be interested in doing static anaylsis to begin with, btu the benefits are definitely available.
* Note that "extra" is in scare quotes because ultimately most of the annotations are usually things you should be documenting anyway, so it's not so much "extra" work as documentation that gets done sooner rather than later. -
Re:None of the above...I've taken a course on this in university. The tools I remember did basically an exhaustive search of all states in your program, and verified that there were no deadlocks and the properties you specified hold in every state.
Needless to say, this is very memory consuming, and can take a long time. So what you really get to verify is simple models, not your actual application with all its different variables. Also, the tools didn't grok Real World programming languages, so you had to write your model in a language other than the one you would eventually write your application in. I can't comment as to what the OP does, but these days there are tools out there that will do the job fairly well. The tools I have in mind tend to sacrifice a little bit of certainty for a healthy dose of speed. That is, they won't guarantee that there are no errors, and they may in very odd cases, flag things that are not actually errors, but they will run fast -- taking about as long as a compile operation would -- and are quite usable on modern hardware. Don't, btw, be too disheartened by the lack of absolute guarantees; while these tools don't offer complete verification, their weakness is more theoretical: they catch many many errors (on par with unit testing for rigour, though often catching different kinds of errors) very efficiently.
As to the question of whether the tools grok Real World programming languages; the ones I'm thinming of certainly do. Usually they take a Real World programming language and extend it with annotations specifying behaviour, and then verify the actual code against the specification annotations.
That means that you can write Java, annotate your with JML and have tools like ESC/Java2 do verification of the exact Java code you are about to compile against the specifications provided by the annotations. Note that you can get Eclipse plugins to integrate the extended checking right into your Eclipse session.
Alternatively, you can write C# and mark it up according to the extended language Spec#, and have a theorem prover verifying your C# code against the Spec# verifications (which are just part of the code really) as you go. This is integrated into VisualStudio; you can see an early version of this at work from 2006 here.
If you're willing to get a little more out there for Real World programming langauges, you also have the otion of using Eiffel with ESpec to provide an integrated workbench of theorem proving, automated unit testing, and acceptance testing in one package. There's also the option of going with Ada and using SPARK; in this case you have to use a restricted subset of the full Ada language, but in return SPARK provides real soundness guarantees.
So I guess the answer is: yes, there are real tools that make this sort of approach practical and integrate well with Real World languages. -
Re:None of the above...
Just to make this a little more clear for the practical minded: the end result can be learning JML, a language that allows for annotations to Java (such as pre- and post-conditions for methods, assignability clauses for private variables, etc.). What benefit does that get you? Well you can use ESC/Java2 to run a theorem prover over those assertions about how things are supposed to work to verify that you code will actually meet all the claims you make of it (which is great for catching subtle unlooked for conrner cases). You can use the jmlunit tool from JML itself to create an automated set of unit tests to exercise you code against your annotations, and you also get (via jmldoc) to have your requirement annotations automatically included in your javadoc api documentation. When you consider that, for a lot of code, you ought to be writing those methods requirements up in api documentation anyway, all the extra extremely rigorous (and static/compile time) checking is just gravy. So there is plenty of practical benefit that's easy to get. To make best use of it, of course, you do need to have some grounding in how this sort of thing works so you can write your specifications well (no different, in many ways, than having some grounding in how CPUs work so you can write more efficient code).
-
Re:Wow.Now just one more thing, guys: make the entire system run on Linux or other F/OSS operating system. If I got to add just one more requirement, it would be that the voting software was formally specified, such that the code can be machine verified against the specification, and properties of the specification can be formally proved. Sure that requires a little more work, but really, if there ever was a place where you wanted the extra assurance of security and correctness you'd think it would be in your voting software. Indeed, it not like this sort of thing hasn't been considered, and even implemented (with documentation of the formal specs), before. I would think a decent level of formal verification of open source voting software should be a minimum standard.
-
Re:It needs serious language supportBy whom? I'd like to look into it for my Java projects. DEC R&D made ESC/Java (Extended Static Checking for Java) that used a theorem prover and specification annotations to verify contracts. Development stopped, but it is now open source as ESC/Java2 which uses JML as annotation markup. I actually listed this as the Java DbC implementation in the article description.
-
Re:Or is it the other way around?
Not only is a lot of history lost and destroyed, a lot of it was flat out fabricated... The mind boggles at what history professors would consider a "primary" source of information.
Hmm.. I wonder if, along with Wikipedia, we ought to ban Herodotus as a cited reference? After all, he is known both as the Father of Histroy and the Father of Lies.
But that's what makes him interesting, in a way. He reported everything he was told, sometimes stately flatly that he thought it was total lies (and, curiously, sometimes giving evidence which mean we NOW know it wasn't, such as the first people to circumnavigate Africa).
But this reporting method of Herodotus - of ALL stories, fanciful or otherwise - does give us a wonderful insight into the world in which he lived.
I wonder if the same will be said of Wikipedia in future times, providing they keep the history of all edits made?
If I live long enough, I look forward to a socialogical and historical analysis! -
Re:Static analysis unnecessary!
Static analysis becomes virtually unnecessary when you use a proper, statically-typed language like Haskell, Standard ML or OCaml. Furthermore, the use of garbage collection eliminates many of the buffer overruns that plague C and C++ software. Add in proper unit testing, and you're almost guaranteed to have a rock-solid system, developed very economically and often with extremely clean code.
As nice as that is it runs into the difficulty that there are already millions of lines of code in Java and rewriting them in ML or Haskell just isn't feasible. If you want a good intermediary position then using JML to specify the existing Java code and jmlunit and ESC/Java2 to do unit testing and static analysis based on the specification can get you a long way. -
Re:You don't ship test code
...unit testing which seeks to build a wrapper around units of code in order to put the code through its paces. It can identify areas of code that are problematic, are never executed, are buggy, or generally are seemingly okay.
If that's what you're using unit testing for then I agree, that's rather a waste of time. If you want to find areas of code that are problematic, never executed (unreachable) or buggy, then you're better off using a static model checker like ESC/Java2 or ES-Verify. Of course both of those require you to specify your code with contracts so they have something to verify against, but then as you say, you ought to be doing that anyway.
Of coure not everything can be completely adequately specified in contracts, and for that you will probably need unit tests, and acceptance tests, or variations thereon. However, as you point out elsewhere, that sort of testing is more the sot of thing that the testing department can handle. Maintaining code specifications as part of the code itself to allow for automated testing and model checking is something you can expect of developers however. -
Re:Easy to write a negative book
Any ass monkey can right a book of criticisms... I would like to see his attempt at a software development methodology that is better.
It is highly unlikely that there will be a particular methodology that magically makes things better, but certainly there are things you can do to make things better. Two major hurdles in software quality are "building the right product" and "building the product right". That is, is what you are planning to build what the users want, and is what you're actually building the same as what you're planning. There's no magic methodlogy, but spending some time thinking how to best answer those questions for your particular piece of software can go a long way toward lifting the quality. The first question, ultimately, is the hardest - working out what you need to build involves wheedling the details out of the customer. You can do things like acceptance testing, or try an agile rapid feedback approach, but that isn't always applicable, and it isn't necessarily going to get you the right answers.
The other side of the issue is a little easier, presuming you're willing to expend a little effort. At the most basic level there is testing - whether that is direct testing from a testing department, unit testing, or automated random testing (like quickcheck or AutoTest). Alternatively you can step up to extended static checking tools like ESC/Java2 or Spec# which use automated theorem provers to try and find potential errors, effectively testing all possible inputs - they can't always find errors, but they can find a great many that testing won't. In the end though all of these, even the most basic testing, require you to be able to specify what it is you are trying to build (see the first paragraph). The more preceisely you can specify that, the more powerful the testing you can do to verify that you're building what you intend. That means the quality of verification is up to the quality of the validation - how well you know whether you are building what you want, depends on how well you know what you want to build. -
Re:In C++
Besides the many very good points you mention there's also the question of documentation - good DbC systems are integrated into the autogenerated documentation elegantly. All that said, you do have more options then Eiffel if you want to use contracts. If you use Java you can use JML which I believe covers all your points, and my point about documentation. If you use Ada you can use SPARK which again, covers your points quite well. Both SPARK and JML also offer (via ESC/Java2 for JML) extended static checking as well as the usual runtime checking of contracts. Finally for C# there's Spec#, but I don't know too much about that one.
Still, Eiffel is actually an extremely elegant language with powerful DbC built into at the core. If DbC is something that's important to you Eiffel probably is your best choice. -
CO2 effects on plants
Most of the people think, that CO2 just rises the average temerature and even this is doubted. Spare me your arguments whether this is the case and if it is man made.
When I was studying, we had a course in plant physiology discussing CO2 levels and the impact on plant growth and how they can cope with changing CO2 levels. While in general it has been shown, that the amount of biomass per area increases up to 40% with doubled CO2 levels it has also been shown, that the ratio between carbohydrates and other nutrients in the plants changes as well and as expected. In other words; insects,animals and humans have to eat a lot more of these plans to get the same amount of e.g. selenium, chromium and others. While humans can supplement their food with vitamins and trace elements( at least in the western world) animals haven't developed these capabilities so far and may not even know about this problem.
See here: http://www.grist.org/news/maindish/2005/07/12/sche rer-plantchem/
Another impact on plant physiology is the number of stomata with which the plants exchange gas, heat and water with the environment. Increasing CO2 levels lead to the reduction of the numbers of stomata, which in turn makes the plants more sensitiv for "rapid" climate change.
See here: http://www.ucd.ie/cabinets/exhibit1.html/
Just two examples, but if you look, you can certainly find a lot more on these issues. There is a lot of fun coming up and most important, if one doesn't understand what is possibly changing or doesn't care, because we can easily solve the problems we create, it will cost lots of money... -
Re:too hard.
By the same token, code checkers can't know what your intentions are for every variable and class relationship. They can tell you if you generate invalid or null variables, or if a function is orphaned, stuff that is strictly boolean. Beyond mistakes like that, you'll have to tell the checker in explicit manners what to look for, negating the benefit of the tool.
If you state your intentions in a language that the code checker understands (preferrably a language designed to be expressive when it comes to making assertions) then the checker can actually determine a great deal about your code. For instance, look at ESC/Java2. By providing annotations to your Java code it allows the checker to find far more errors than the small amount you suggest. Developing using ESC/Java2 instead of a compiler to "check" your code can be very productive (it checks Java syntax and does type checking as well, so if it passes ESC/Java2 it will definitely compile) - Things get flagged as potential errors early on, often forcing you to add extra annotations to clarify your intentions (which is a good thing! it often helps you actually flesh out your ideas of exactly what you intend), and by the time you're done the odds of code working as you intend is far far higher than you would ever expect otherwise.
The fact that the annotation language that ESC/Java2 uses can also be automatically included into your JavaDoc documentation (making method requirements explicit, and making clear what a method guarantees), and can also be used to automatically build a JUnit testing framework for the code - well that's just icing. Take a look - download the Eclipse plugins here and here and try it out. I think you'll be remarkably suprised how powerful the error checking is, and how productive the development cycle can be when using it.
Jedidiah. -
Re:static_analysis++
Also, back on topic, try writing financial software some time. It's like a different world. Everything is unit tested, and the unit tests don't so much check for bugs as prove that your code works.
Unit tests don't prove your code works any more than drawing a few right angled triangles and measuring the sides proves Pythagoras' theorem. If you want to prove your ode works you use a theorem prover. To do tht you usually need to provide more detailed specification (beyond just type signatures) about how your code is intended to function. That tends to be more work, though if you really need to know your code is going to work it can often save time in the long run (over ridculously long and exhaustive testing). There are things out there that provide toold support for theorem proving aout your code: SPARK Ada along with the SPARK tools provides a powerful theorem prover, and HasCASL with CASL tools (including the HOL theorem prover) provides string theorem proving for Haskell. Even ESC/Java2 utilises a theorem prover (called Simplify) to provide extended static checking of Java code. I'm sure there are more examples.
My point is not that Unit testing is bad (it's very good), but that you shouldn't overstate its effectiveness. Unit tests are a great way to provide a reasonable degree of assurance that your code will hopefully ork as intended. It isn't a substitute for actual assurance however. It really depends on exactly how sure you need to be - how much an error will cost, and whether that can be tolerated.
Jedidiah, -
Re:static_analysis++
If you want a truly powerful Java static analysis tool consider ESC/Java2 which includes not just the usual extra static checking you would expect, but also includes a theorem prover which can provide warnings for all kinds of deep and subtle errors. Read through this presentation (warning PDF) to get an idea of exactly how many things ESC/Java2 can catch, including warnings about race conditions and deadlocks. If you want powerful statsic analysis of Java code ESC/Java2 is definitely the way to go.
Jedidiah. -
Re:the "pet rock" of programming languages
Design by Contract is particularly nice if you are willing to spend a little extra effort to write very reliable code, but it would be even better if there were good theorum provers out there to verify that contracts will always hold and warn if they don't. The would be much more developer friendly than the predicate calculus normally associated with formal methods.
If that's what you're looking for then I would suggest that you take some time to check out JML and ESC/Java2 which provides almost exactly that functionality for Java. It's not as clean as Eiffel as the contracts have be be kludged into Java as add-on annotation in comments, but all the functionality you'd want in a good expressive DbC system is there in JML, and ESC/Java2 provides a static checker/theorem prover that can attempt to verify contracts and provide warn you when they might fail. It also provides a number of other strong static checks based on JML annotations, allowing you to have high degree of confidence in well annotated code that passes ESC/Java2. Honestly, download JML, JMLEclipse and ESC/Java2 and try them out - you'll be amazed the number of subtle errors that can be quickly and efficiently caught!
His belief that a method should never return a value and have a side effect is particularly bad. Writing a stack with get_top() and remove_top() instead of pop() is a little weird.
It seems odd, but it does have nice aspects, particularly if you're used to a more functional perspective: it goes a long way toward isolating side effects and allowing better reasoning about the scope of effects that a given block of code may have. It certainly makes sense to me.
Jedidiah. -
Re:Dynamic typing
I'm firmly in the static typing camp. Not only does it make things more reliable (due to compilers catching errors)
There's a lot more in the way of errors that can be caught statically with very little extra effort - you just have to use a different tool (one specifically designed for the task) to check for errors statically instead of the compiler, and provide a few appropriate hints about your intentions (in a language that's very expressive for stating your intentions) as you write your code. For Java the tool is ESC/Java2, a very powerful static checker. It will catch all the errors a compiler will, plus a vast array of potential errors that mere compilation will never spot.
If that sounds good, then it's worth pointing out that the extra annotations you need to add to explain your intentions can also be automatically converted into runtime assertions during the etsting phase, can be used to automatically generate JUnit unit testing frameworks, and can be automatically included into your Javadoc documentation. For the small cost of adding a few extra annotations - things you would be documenting elsewhere anyway - you get far better static checking, a powerful testing framework and harness for free, and it all goes into your documentation automatically.
Check my sig, or head directly to the JML website to get an idea of what can be done.
Jedidiah. -
Re:Dynamic typing
For the amount of time that i've lost to define a method twice to deal with 2 different types of objects, i've saved tons of time dealing with bugs that result from dynamic typing.
And just think of the extra time you can save by adding a few annotations to your code and allowing a static checking tool like ESC/Java2 or Splint catch all the extra errors for you. Better yet you can get tools that will extract that extra documentation of the method out and include it in the automatically generated documentation - making it much easier to keept your documentation exact and up to date.
Jedidiah. -
Re:Ah. Dynamic typing. Again.
To me static checking (that is consistency checks that are done at compile time) are like an Engineer designing a plane, he does it with tools that declare the wings and the parts of the plane sound, even before the tests that have to be done to confirm the project.
And I think something that static typing advocates who use this sort of argument need to realise is that static types are not the be all and end all of declarations you can make to ensure consistency with intended function. In theory the Curry-Howard isomorphism means that indeed types are propositions. In practice most type systems provide a very poor syntax for clearly stating your propositions. The best way to get around that in most languages is to provide extra syntax that allows expressive descriptions of your propositions, or, if you like, your assumptions. Yes, the type signature of a function declares certain properties that ensure a certain amount of consistency that can be checked statically. There is a lot more in the way of assumptions you can decalre that will ensure far more important consistency properties that can still be checked entirely statically.
Check out JML and ESC/Java2 for Java to see how much extra static checking you can get above and beyond simple type checking. The same sorts of things for C are provided by Splint. If you're someone who prefers ML then take the time to check out EML which adds the ability to define and check axioms in Standard ML.
Jedidiah. -
Re:Totally fresh in programming
counter = 1
in a statically typed language that is picked up at compile time. in a dynamically typed language you won't notice it until your app hangs at runtime and you'd better hope your in a situation where you can easilly attatch a debugger.
while counter < 10:
do something...
couner = counter +1
In some ways the confusion here arises from the fact that static types had benefits in optimization, and hence were necessary information for the compiler to parse correctly. At the same time static types are used as a means of checking (to a certain extent) the correctness of code. Because the compiler ends up doing the correctness checking because it needs to sort out the types it has become common to conflate compilation and static error checking into a single task, when really they are two quite separate tasks. What am I getting at here? That compiling or interpreting a program isn't really how you should be checking for correctness - it's nice but hardly necessary. If you ran python static correctness checking tool pychecker (which tries to statically catch many common errors) over that code it would throw a warning that "couner" was set but never used, happily catching the typo/spelling error. In fact if statically checking your code is important you'll find pychecker will catch a great many common errors for you.
Now as to the separation of static checking and compilation - if you're willing to see that static checking is a separate task and devote tools to just doing that then you can do a whole lot better than just static types. Check out JML which, by adding extra annotations beyond just static type annotation, allows you to use far more powerful static checking like ESC/Java2 which makes standard static type checking via javac look as poor at catching errors as a dynamically typed language.
Jedidiah. -
Re:The numbers are unimportant
It really depends on what you are writing. If you're implementing a security protocol, or a network service, then taking the extra time to spell things out and be able to prove there aren't any buffer overflows is probably entirely worth your time.
For projects that aren't as critical you can still get significant benefits from a slightly scaled back approach - things like Design by Contract help developers to spell out their intentions more clearly and can go a long way toward catching and isolating bugs earlier. If you're using the right tools (like, say JML combined with ESC/Java2) you can even do extended static checking and catch a lot of other bugs, where what you've coded doesn't match your stated intentions (usually in the form of annotations) much, much earlier.
No, there's no silver bullet. That doesn't mean, however, that there aren't things that can be done that make things better than they are now.
Jedidiah. -
Correctness-centric development with JavaIf any of you are interested in using the practices that Praxis preaches but you are working in Java, I suggest researching the Java Modeling Language (JML).
JML is a formal specification language for writing contracts for your Java programs. (It has nothing to do with UML or XML, other than sharing two letters.)
There are a number of quality research tools that understand JML including a compiler (jmlc), a documentation generator (jmldoc), a unit test generator (jmlunit), and an extended static checker (ESC/Java2), a kind of automated theorem prover, like FindBugs on steroids).
These tools and technology let you do design by contract and contract-based unit testing in Java 1.4 and are used by many universities and companies to help them build quality software. See the ESC/Java2 FAQ for more information.
Disclaimer: I am part of the research community that develops JML and the co-author and maintainer of ESC/Java2.
Joe
-
Correctness-centric development with JavaIf any of you are interested in using the practices that Praxis preaches but you are working in Java, I suggest researching the Java Modeling Language (JML).
JML is a formal specification language for writing contracts for your Java programs. (It has nothing to do with UML or XML, other than sharing two letters.)
There are a number of quality research tools that understand JML including a compiler (jmlc), a documentation generator (jmldoc), a unit test generator (jmlunit), and an extended static checker (ESC/Java2), a kind of automated theorem prover, like FindBugs on steroids).
These tools and technology let you do design by contract and contract-based unit testing in Java 1.4 and are used by many universities and companies to help them build quality software. See the ESC/Java2 FAQ for more information.
Disclaimer: I am part of the research community that develops JML and the co-author and maintainer of ESC/Java2.
Joe
-
Re:I have to wonder....
Thanks for a thoughtful post.
And why are softwares so buggy and have such a lousy reputation anyway? Not to start a flamewar, but let's just list a few possible "reaons" here:
I think, to be honest, that it is a combination of a number of the factors you mention.
Why aren't schools teaching this methodoly thoroughly? Why aren't this toolset and programming language taught in school by default?
To do proper formal specification, one of the key parts of Praxis' Correct by Construction approach, does require a decent solid mathematical background. I think a lot of CS departments, facing students who want vocational training, struggle to demand the sort of mathematical requirements that are needed. As to SPARK - it is something that Praxis developed themselves, and it is proprietary (the toolset at least, the annotation language is well documented). You can pick up a book and learn the language, but the tools cost money if you want to use them commercially. On the other hand, the base specification language Praxis uses, Z, is entirely open, and there are a variety of freely available tools for it. There are also other specification langauges (I quite like CASL which has a number of useful extensions) that have freely available tools associated with them. There's also JML and ESC/Java2 which are freely available and seek to provide the same sort of functionality or Java that SPARK adds to Ada. There are places that teach JML, but they are still few and far between.
Programmers are asked to do the impossible.
I think this is a big part of it in some ways. Partly this is because, for a large number of software projects, the degree of exactness and quality just isn't required. I don't need a professional architect to help me build a doghouse in my backyard (though I'd certainly want one if I was building a skyscraper), and I don't need assurances of bug free software for a simple web front-end to a database. At the same time programmers are often unwilling to let customers know exactly what the limits are when developing software. To quote you: "If a customer dares to ask a civil engineer to add 2 more stories between the 3rd and 4th floor after the custom-built building is finished, guess what would the civil engineer say?"; if software engineers aren't prepared to stand up for quality and tell customers that somethings can't be done without sacrificing the quality of the product the problem will remain. In part I think this is due to the fact that software development is a young industry, and programmers are still of the mentality that they need to do everything they possibly can to please a customer. Partly it's because software projects are diverse (as are building projects!) and sometimes it's okay to make late changes; sometimes it's how things ought to be done - the key is to identify exactly what sort of project it is as early as you can. Are you building a treehouse for your kids, which doesn't require exactness and benefits from incremental design and feedback, or are you building a 4 story building where quality is important, and late changes will jepordise that?
Programmers are a bunch of bozos who know shit about proper engineering.
Sadly this is partly the case. There are an awful lot of cowboys out there when it comes to software engineering. There are, of course, a lot of fantastic programmers as well who are otherwise beset by some of the other points mentioned. There is, however, a remarkable degree of tolerance for cowboys, sloppiness and lack of quality in software engineering that you don't see in other engineering disciplines. Partly I thin -
Re:Give my regards to the Earth's core...
Problem solved.
http://www.ucd.ie/ucdnews/apr00/mystery.htm
or for people who like equations:
http://www.copernicus.org/online-papers/EGS/NPG/20 02/3/npg-9-373.pdf -
Re:Open Source VotingFrom what I have witnessed, most American research groups are unwilling to tackle this problem with pragmatic, practical, high quality solutions. In other words, no one on that side of the pond is writing a high quality, fully documented, specified, tested and verified Open Source electronic or Internet voting software system.
Most American researchers and activists, from my point of view, like to complain a lot, but not "put their money where their vote is."
The systems I have seen so far, like the one you cite, are far from ideal. Most are written by a bunch of enthusiasts with little to no experience in developing robust, extremely high quality, complex software systems, and very few of them have any experience at all in voting systems. I.e., they are a bunch of hacked together Perl or Python that barely runs, let alone is the foundation of a future high-quality open source voting system.
This is (partially) why my research group here at UCD is working on these systems. See my prior comment in this article for more details.
-
Re:Swiss Internet voting built on two-factor autheActually, you are incorrect. The world's first national vote took place in the Netherlands in June for the national and European Elections via the use of the KOA voting system developed for the Dutch government.
This system has since been open sourced under the GPL license and my new research group here at University College Dublin is working on completing, documenting, evaluating, and formally specifying the system.
I led the evaluation of this system's external network security for the Dutch government while at the SoS Group at Radbound University Nijmegen.
I was also the co-author of the vote tally application for the European Elections in Holland. That application was written in less than eight weeks using formal methods to ensure that the software of extremely high quality and indeed every vote was counted. This system was written in Java with JML annotations and was partially statically checked (verified) with ESC/Java2.
See the paper "Electronic and Internet Voting in The Netherlands for more high-level information.
-
Vindication of James Lovelock ?
James Lovelock was the guy who invented the current notion of 'Gaia'. Whether you agree or disagree with that idea I think you'll find the origin of it interesting. He was hired by JPL to devise ways of finding life on Mars. So he asked the question: How could we tell there is life on Earth ? And being a chemist he concluded the atmosphere is a dead giveaway. The oxygen in the air indicates life, so with a powerful telescope (he actually wanted to build a 1,000 inch scope to find life on the planets via atmosphere chemistry) you could find if life existed. His argument was not to look just for oxygen but to find if the atmosphere was far from chemical equilibrium
... that would be the telltale sign. Needless to say NASA was not impressed with the idea that they didn't really need to go to Mars to tell if life was there.Here is one link. Doubtless there are others.
-
Re:The whole University System is a racket
I note from your post that you are going straight from school to teaching. I think you make my point that "those who can, do, those who can't teach". You would do your future students better service by getting experience outside the ivory tower before purporting to tell them what they need to know to succeed there.
Q.E.D. (Quod Erat Demonstratum, That which was to be proved).
BTW: Since it seems to be the presumption of most respondents that I am some non-professional ignoramus: I went to College. Actually to two: one the idiot Liberal Arts kind with the spoilt upper middle class party kids predominating that is typical of most ( Providence College), the other a real University that taught, because it had a coop program, and its professors were all involved in industry ( Northeastern University). My father, after a career that involved being VP Of Ops for IBM, and then CEO of 2 phone companies, is now an MBA professor at a major national university in Europe. He shares my disdain for most of American third level education.
I reiterate my point: most "College" is a self perpetuating scam to separate people from their money for the benefit of the mediocrities, who have no real world experience, that run it. The elevation of it to a government subsidized requirement for all but the most menial jobs short changes the K-12 system (of money), most people who attend it (they wind up in debt for no good reason), employers (because they still need to actually train people who have college degrees, only they have to pay them more while doing it because they have grand expectations), and the economy (by wasting tax $ and postponing the changeover from tax burden to productive citizen of a substantial portion of the population).
In short: Too many people go to College, there are too many colleges, most of them learn and teach nothing of much use, and the money spent on it could be used far better reforming the K-12 system. -
iPod mini wheel sound familiar?
A bit ike this?
I knew they'd never move from their one-button-mouse position. If it's enough to make a spaceship land then it should certainly be good enough for everything else.
-
Re:The solution is: FLY NAKED!!!
This is a terrific solution however it does seem to invade our right to privacy. Is Peace of mind is worth seeing naked bodies of various proportions?
This wreaks of stepping on our unalienable rights. Why should our God Given rights to privacy be so unalienable? Liberty Essay
Why should we fight for our freedom?
Dred Scott's fought
The advance of freedom is the calling of our time.
Because if we don't fight we will continue lose it. Like the frog in the pot, it will slowly heat up and we will boil in your loss of freedom. Like the Nazi's took away the rights then more rights then until they finally found it convenient to take away the right to live. You would think we would have learned something. But no. We are sheep.
The terrorists caused more harm to us by causing a societal Auto Immune Disease than by their attacks. The lymphatic system of our society over- reacted to the threat to the point where the true threat is fear which for some reason, our society has propagated. The true problem was the sheep.
We need to teach our citizens to defend themselves from terrorists. We should all learn Krav Maga in grade school. But we would rather be sheep. Fat fast food eating, non-exercizing Sheep that watch too much TV.
It starts with fear. Fear is the mind killer. is the mind-killer.
Terrorists work to create fear. These terrorist succeeded in stirring up a lot of fear. Now we have to fly naked.
America used to be the Home of the Brave . We did not have fear. We were the land of the "NoFear bumper stickers"
But now we fear our fellow americans. We fear anybody we don't know who rides on the airplane with us. We fear men in turbans. We are afraid to lose our valuable sheep lives.
This is why we should be able to bear arms. An American with a machete, a machine gun, a nuke, and nifty ice9 nano particals is a Free american afraid of no one. The interesting aspect of this is that if one bears arms he is afraid of something otherwise why carry the extra weight? We should be able to bear arms but we should not because bearing arms shows that we are afraid. What arms we decide to bear is irrelevant.
Q. What are we afraid of?
A. Death, loss of life, loss of loved ones.
Q. Why are we afraid?
A. We are afraid of where we go when we die.
1. heaven? if we are going here,
what are we afraid of? cool gardens streamside with plenty of fruit? Spending eternity with our God?
2. hell? if we are afraid of going to hell we are already in hell.
3. nowhere? Ceasing to exist is like total loss of freedom. We are afraid of losing our freedom. Why give it up without a fight now. Why die the little death?
Sheep.
We are sheep.
We go where they say to go.
When they say submit to the search, we submit.
When they say bend over, we bend over.
When they say no nail clippers, no baby swiss army knife, no pointy things, do we say "We are free!!! We are CITIZENS!!! WE HAVE UNALIENABLE GOD GIVEN CONSTITUTIONAL RIGHTS TO BEAR ARMS/FINGER NAIL CLIPPERS!!!!!
When they say "fly naked", we will submit.
When they say take this tattoo on our hand or forehead, we will submit.
Why?
Because we are sheep.
When they say we will implant rice chips in all our kiddos when they are born and we will track their GPS coordinates and purchases for their lives, we will submit. We won't just submit, we will want it. We will demand it. Why?
Because we are sheep.
Be brave and be free. Remember the Su -
The Best of All Possible Worlds
'Monads' are part of Leibnitz's philosophy, which Voltaire famously satirised in Candide with the figure of Dr. Pangloss, who resolutely maintained that we live in 'this, the best of all possible worlds' despite a succession of disasters that would convince any sane man that he was wrong.
How very suitable for a Microsoft product.
-
Alt-Gr (as seen on lusenet)
Alt-Gr, useful when that regular "Grrrrrrrr!" just isn't enough.
(Alt-Gr key example (in this case being illustrated as part of a key combo to produce the Euro symbol)) -
Re:ccTLD whois
You are porbably addressing the exact arguments of the ccTLDs with your statement! What if a country does not wish to have a whois service? Your approach is that they must, the countries is that it is up to them to decide whether or not they want to implement it. Look at this page to see how EU laws regarding data protection made the Irish domain registry remove whois. If we have one world government to rule them all then perhaps we can start to allow ICANN (or their replacement) to govern all the TLDs but until then each ccTLD should be allowed to run intself under any rules it desires. If China/France/Namibia chooses to make their TLD incompatible with the rest of the world why not? DNS is not TCP/IP and as long as a network complies with TCP/IP standards then it is on the net regardless of whether or not they use a DNS system at all or even one which is compatible with the rest of the net. It is up to each hostmaster to determine how they want to progress and whose rules they wish to submit to for any dns resolution they may require.
-
Re:Have Motorola's chips really lagged behind Inte
When you get right down to it, Intel and AMD fans really do believe that the performance rating of the CPU is its clock rate.
Okay, tell me what processor is faster than the current high end AMD or Intel processors? Please feel free to link examples of single processor competitor systems that trounce the high end AMD or Intel options on widely respected benchmarks. The reality is that the el-cheapo $200 Althlon holds its own and surpasses the majority of lauded, super-duper "RISC" (I use that laughably as most users of the term seem to have pulled a PC Magazine out of their 1988 archives, and don't understand the current state of processors) processors, but fans of UltraSparc, Alpha, etc, presume superiority just because it's rare, sort of like how the anti-Pop are sure that their particular music favourites are superior because they're "alternative".
As far as clock cycles/instruction, all current processors have superscalar instruction pipelines and generally perform at least one instruction per clock cycle (20 or 30? Geesh, you looking at an 8088 timing book?). -
Re:Cue the inevitable ...
>A check on historical inflation rates shows that $5.50 in 1982 is the equivalent of about $10 today.
Computers have not followed inflation rates, though.
A Sinclair cost $149 at introduction. It did hooked up to a TV, so a purchase of a monitor was not required.
Today, a decent PC will cost $600 + $150 for the monitor. That's $750.
That's 5 times inflation in the computer market.
$6 x 5 = $30.
That's what I was basing my pricing differences on. Inflation rates only seem to work well for steady commodities and housing. -
Some DVD info.Here are some links that you may find useful:
- DVD and Linux Support
- LinuxVideo.org
- OpenDVD.org
- Sigmadesigns Product - they have couple DVD products that you may find interesting. NetStream 2000 has Linux drivers (BETA) available on their FTP site.
- Linux DVD from Liberty Surf.
Hope this help.
-
Re:It's all Greek to me
For further applications of Perl to ancient Greek and to Latin, see here.