I'm going to assume that you accept the premise, but don't see how it proves the conclusion. If you actually don't get the premise either, you'll have to read the proofs ("it has been shown..."), or just accept that since all computer programs are expressed as a finite-length string of bits, those bits can be interpreted as a finite integer.
Here's the proof.
Since we accept that all computer programs can be mapped to integers, it follows that every program that computes a number (a strict subset of all programs) is mapped to an integer. Construct a mapping which takes the number and maps it to the number of the smallest program that generates that number.
Of course it will. This is a universal problem with ALL power generation and use. It can be reduced ONLY by increasing the efficiency.
Again, this is universal. There's no energy production system that's immune to it. Further, the amount of the increase is related to the amount of power produced, NOT the type of energy source.
Radiation would turn the usual high temp-high pressure tubing into something with holes resembling swiss cheese in a few years, so some exotic materials need to be used - and replaced every now and again.
I'd like to say I know you're wrong, but I don't. It just doesn't sound right to my half-trained ears. Could you provide a reference to explain this? Feel free to make it a technical one; I'm not an expert, as I mentioned, but my degree is in chemical engineering (although I work as a programmer), so I can follow it.
The rest of your post seems equally suspicious to me, but the one part I'll speak up against is your comments about steam. There you definitely have no clue on what you're talking about. Simply because steam was used for transmission of power a while ago does NOT make it primitive; on the contrary, it makes it (relatively) mature. Because it's so widely used, its properties have been very well explored, and efficiencies of systems using it are extremely high.
Yes, it would be powerful if it were true. Warning: don't assume it's true just because you want it to be.
Von Neumann established the neccessary complexity for an organism to be capable of evolution: it has to reproduce, self-diagnose, and self-repair. If it can't reproduce, it won't possibly evolve; if it can't self-repair, it won't have enough 'genetic' stability to evolve; and if it can't self-diagnose, it can't conserve energy by performing repairs only when needed. The size of these creatures suggests something below the previously known size threshold for these functions, which indicates a possibly lower complexity.
These might indeed show us a possible path to life as we know it, thus providing the first evidential path for abiogenesis. (The Miller experiments were fine, but only showed what/could/ happen in highly hypothetical conditions; furthermore, their results were pretty useless to explain anything more complex than the most simple assemblies.)
So I think a lot of people will be watching these. I certainly will -- but I'm not holding my breath, either.
SPARK's assertions differ from C's because SPARK's are gueranteed to be complete and correct, otherwise the verifier won't let you past.
You could, in theory, use to do design by contract, but you'd have to be very careful to put your assertions in the right places, make sure that none of them have side effects, and manually do a few other things that a DbC language automatically takes care of for you. It'd be risky, but it's possible. It becomes MUCH harder when you add object orientation, though; managing inheritance of invariants becomes very difficult.
Your point that "correctness isn't always necessary" is well taken. The more you need the more you have to pay, and not every project can afford the price.
The rest of your post absolutely requires the absence of a tool like SPARK. Throw SPARK into the mix, and all your grounding assumptions are absolutely wrong -- the specifications _do_ describe the interfaces, and the interfaces _do_ work together, and the code _does_ implement the specifications, and there are no possible exceptions.
Trivial examples all show the benifits of whatever new language feature has been added. It's really only after significant use and experience that we can judge how good something is in a large scale appplication.
So tell me -- how long has SPARK been around? How many projects has it been used in? With what level of success?
Are you judging it without knowledge?
I remember getting excited about the "Z specification" language in 1986, but in the end it was just too damn hard for everyone. The programs were absolutely correct but if you wanted to change something later, you were back to square one. Forget about anything large involving multiple people.
I've seen it used too. And I agree.
I find SPARK different -- rather than a mathematical expression of operation, it allows you to build a mathematical specification (which is easier), and tie it provably to a computation (which is fun). It's still not easy, but it's easier.
Give me a sandbox, lego bricks, and let me play.. go away I don't like your rules.
No problem. I don't like embedded programming; some people do.
So that fact that Ada had DoD funding for a denotational semantic specification and Java does not does have such a specification does not make Ada more portable and reliable (in the sense that a piece of code will produce the same result on different platforms).
You're right that the phrase "formal specification" was a bad choice on my part. Ada doesn't have an official formal specification (although SPARK does); what Ada has is a highly formal official specification, automatically verified by an extensive validation suite that every compiler must pass.
This official requirement made writing Ada compilers VERY hard (a big reason why Ada wasn't successful), but it also makes it possible to write unambiguous formal semantics for a clean, useful subset of Ada. This is what SPARK uses.
And SPARK does formally guarantee precisely what you claim it can't: that a piece of code will produce the same result on different platforms, and even on different compilers. Once you've verified that the code is valid SPARK, you also know that it's valid Ada, and that it's totally and purely portable. No annotations or theorem proving needed.
Choosing Ada as the basis for anything guarantees that few people will use it.
That's easy to say, but there's no choice here. It was Ada, an ad-hoc language, or no solution at all. Put that way, the choice is extremely simple.
I would argue with your statement on other facets, but you've left it ambiguous enough that you could claim it's correct no matter what the facts are. (All you have to do is say, "That's not what I meant by "few people.") Let me just say that SPARK appears to be the only product in its solution domain -- that is, there's no choice if you need to be 100% certain that your code won't throw an exception and give you an Arianne 5.
The module paradigm for languages (used by Ada and Modula-2)
Stop right there. Ada doesn't use "the module paradigm". It's a full-power object oriented standard, and has been since Ada 95. It's had genericity and static polymorphism since the original Ada.
Finally, just because you have a specification and code that exactly implements this specification does not mean that the application will not result in unintended results (e.g., the death of users or others).
There's no doubt of that. Or those results may have been the INTENDED results (military applications) -- the compiler can't tell the difference.
So I have to agree with you.
Frequently the problems encountered with software are a result of conditions that the designers did not forsee. That is, things that were not defined in the specification.
But using SPARK does mean that you DON'T have "problems encountered with software." If you have a problem, you know good and well where it came from -- bad specifications, not bad software. That's a huge improvement, wouldn't you agree? Narrowing down the location of the fault is the first step toward fixing it.
Er... Read my message again. I wasn't knocking Eiffel; on the contrary, I was giving Bertrand credit for having DBC nailed before SPARK came along.
I also wasn't talking about Eiffel's support for DBC; I was describing DBC in general, or more accurately DBC without OO support. I didn't claim that OO isn't possible with DBC (on the contrary, I stated that it was, and I would explain it if asked). I didn't claim that Eiffel didn't have OO.
And finally, the huge thing that's new in SPARK that isn't in Eiffel is static contract checking. That's not present in Eiffel, for all its wonderful features.
This seems rather a waste of time. You either first describe exactly what the code does, then write the code, or you write a simplification of what the code does, then the code.
It's not a waste of time to describe what a function does. It's essential to keep "what" a function does distinct from "how" it does it. That's the whole point of interface versus implementation.
Consider a function with the following contract:
function: sqrt( x ) preconditions:
- integer (x)
- positive (x) postconditions:
- result > 0
- result * result <= x
- (result+1) * (result+1) > x
Now, can you see how that's useful? And do you see that this tells you something _completely_ different than what you'd know if you read the actual source code for that function (perhaps an implementation of Newton's method)?
In the second case, your specification does not cover every aspect, which introduces loopholes, defeating the purpose of the contract.
That's what SPARK's automatic verifier is for -- to prove that there are no loopholes.
I would have been interested if all this instrumentation had been grafted onto a language like Java, or C++. But to have to switch to Ada just to be able to add in instrumentation that helps in code analysis?
Switching languages is a tiny effort compared to the change required to design your code for static validation. The SPARK people strongly recommend against trying to "switch" to SPARK; if you want the benefits, you have to code with it from the start. It's kind of like taking a 100,000 line C program written by 30 programmers over 10 years and trying to "switch" it to C++ -- it's theoretically possible, but in practice it's easier to start over.
And what they did in Ada would have been impossible in C++. It's significant that SPARK code will run EXACTLY the same on all compliant Ada compilers. No platform dependancies, no ambiguities, no undefined behavior... ALWAYS the same. You simply can't possibly define a subset of C++ which would be able to make those promises. I don't know if it would be possible with Java; since there's no formal specification of Java, probably not.
It's also funny that he WOW's at the idea of no dynamic memory allocation...
I felt that way too:-). Odd.
The reason they did it is simple, though -- they wanted to be able to set absolute bounds on when a SPARK program will or will not fail (throw an exception). There's no way to do that with dynamic memory allocation as it's defined in Ada and most other languages.
Yes, that's limiting; no argument. But for some problems, particularly ones solvable by programs managing their own memory, the limitation doesn't matter compared to the benefits -- a SPARK program can execute without any runtime support code.
Why not just use a type safe language?
No such thing -- type safety is an uncomputable problem.
If you meant strongly typed, that's easy; Ada was already strongly typed. SPARK just guerantees that the programs will always run the same, and SPARK's verifier guarantees that the types are chosen and described correctly.
Design By Contract was not invented by SPARK; the name was popularised by Bertrand Meyer, who added it to his "Eiffel" language.
Anyhow, DBC is totally distinct from object orientation. In DBC, each component in your software comes with a "contract" that states "if I am called when the _preconditions_ are true, I promise that after I run the _postconditions_ will be true."
The preconditions and postconditions are a group of logical statements, hopefully ones which are useful to your program:-).
Let me give a little example.
function: sqrt( x ) preconditions:
- integer (x)
- positive (x) postconditions:
- result > 0
- result * result x
Do you see what's happening there? Without knowing/anything/ about how sqrt is computed, you can use it in powerful ways. Preconditions and postconditions can't always be as informative as the ones above are (the ones above define everything about the integer sqrt function), but they can give useful information.
Adding in object orientation support to DBC is a little more complex, but I won't go into that unless asked.
Traditional DBC systems, including Eiffel, couldn't verify your contracts, so most of them would translate the contracts into code, and include that code in the executable; if a contract failed, the code would throw an exception or otherwise fail. SPARK is interesting because it can detect contract failures without running the code; it can also detect when your contracts fail to promise enough.
Patenting itself doesn't break the GPL. Patents without freely available licenses would do so, though.
IBM, for example, is talking about opposing software patents. They could set a shining example -- put their money where their mouth is -- by taking a first step and licensing some of their software patents for unrestricted use under the GPL.
Such a patent license would definitely meet the demands of the GPL; in fact, it would do the same thing to patent law that the GPL does to copyright law.
I wonder how all the peace mongers would react if Hitler (the original, not some barely literate moron with a Texan accent) was alive today. You'd probably just let him be (unless he was American or Israeli.)
Don't spend too much energy wondering -- just read history to find a confirmation of your suspicions. The overwhelming sentiment in America before Pearl Harbor was antiwar; Americans saw Hitler as just another cruel, powerhungry dictator on a landmass full of cruel, powerhungry dictators. They weren't interested in entering yet another expensive war to help a group of nations that were still engaged in avoiding repayment for WWI debts. Charles Lindbergh wrote in this vein; his work is interesting.
He changed after Pearl Harbor, though. Almost the entire nation did.
There are no tests that differentiate between heliocentric and geocentric either. It's purely a matter of notational convenience.
This seems to be a fundamental property of the universe, not a matter of missing knowledge. Any point in space and time can be selected as the origin, and all the equations will work out exactly the same. Moving points are different, but the differences don't allow you to establish preference for one point (the Sun) above another (the Earth).
Nope, that's the case; no Windows clients yet, and none in sight. It's possible that were one to be written, it wouldn't be very good at compatibility.
Use darcs instead if you care about cross-platform bitkeeper-like version control.
What you really need is an engine that is connected only to a generator and always runs at a single speed and always the same loading.
That's a clever idea, but you'll pay more for it than you gain. Yes, your engine will be more efficient; but the overall system will generate more losses (or simply not be usable) because it can't get the output it needs from the engine. Remember, gas is still the most efficient source of power, even in a hybrid with regenerative braking. Storing energy in batteries, or converting from mechanical to electrical, wastes a LOT of energy (although it's better than throwing the energy away).
The Toyota has an interesting twist on this, though. Its engine obviously doesn't always run at the same speed and loading -- but it does always run at its optimal speed and loading. It does this by modifying its cylinder geometry on the fly. Essentially, if you only need half the power it only uses half of each cylinder. (Not to be confused with disabling cylinders -- all the cyclinders keep working; each one changes its power curve. Read more.
No, actually it's the result of a thorough understanding of arch as a result of comparing it with a LOT of other SCM systems. But you can get the same result as me by reading the arch manual, which discusses creating a new archive. Note that creating a new archive is distinct from creating a new workspace; a workspace has to be associated with an archive.
In other systems, including BitKeeper and darcs, creating a new workspace is the same thing as creating a new archive. They are truly distributed; there's no need to tell it which archive it'll be using, because the answer is "the one I'm working in right now". Every workspace is its own archive, every archive is its own workspace.
The difference is astounding -- it's like the difference between CVS and arch. And yes, I was an arch fan, I even converted someone else to arch. He uses darcs now, just like myself.
SVN also compares poorly to BitKeeper and its kin. The problem is that SVN, like CVS, needs to have a configured central repository; BK doesn't.
There are some good free software alternatives; the only one I know of that works like BitKeeper is darcs. (Arch is very close, but it still requires you to configure a central archive.)
Can you compare it to darcs? (I can't, because I've done some work on darcs and am not willing to pay money just to do a simple comparison.) I ask because the way you describe BitKeeper sounds pretty much like darcs.
(Except for the graphical utilities -- I'm told that darcs has an experimental graphical merge, but that's all right now.)
I suspect others will comment on this too, but there are other close equivalents in the free software world.
Arch is groundbreaking, but it was designed in a rather ad-hoc way, and it _really_ shows. You have to know a lot about the implementation details in order to get stuff done in it.
Darcs is much, much easier to use, and is supported on more platforms (including win32). The shortcomings include slow execution time (due to a complex merging algorithm that's part of the reason it's much easier to use) and an unusual implementation language (I like Haskell, but I recognise that many people don't know it).
OpenCM and Monotone are in much earlier stages of development, and I haven't tried to use either in a production environment.
Bitkeeper still has one big advantage: it's got killer graphical utilities and it's really complete. Both arch and darcs are still growing into their full statures.
But I strongly recommend darcs. I don't see any reason to use any other SCM tool, honestly -- darcs _just works_ and is free. Copy the executables into your path, type 'darcs inittree', and start working; it's just that easy. No worries about file identities, no worries about archive locations; it's all taken care of thanks to a well-thought-out model.
Regression tests are also useful _with_ a bug report -- they're a formal reproduction of the reported bug, and once you narrow down the cause they're also a proof of the accuracy of your judgement.
Actually, though, I use them mainly as what I call progression tests. Whenever I think of a feature or design point, I try to express it as a simple test. Then I add to my software code to pass that test. Tests don't hinder my work anymore; they help it along. Rather than the phycological disappointment of doing _additional_ work writing tests only to have my already-written software proven incomplete, I get the psychological reward of having my already written tests tell me when my work is done.
My point: regression tests help on many parts of the software life-cycle, if you use 'em.
I always thought it was because they undercut the local competition and strong-armed their suppliers.
I don't have to deny that (and in many cases I can't; it's obvious historical fact). Strongarming suppliers DOES give Walmart a minor advantage, so it makes sense that they've used it. But that doesn't change the fact that they HAVE used inventory control more efficiently than any of their competitors, and that this efficiency translated into lower prices and produced their overpowering dominance. Without the efficiency, they would have NO dominance, and thus no ability to "strongarm" suppliers.
Slashdot Mirror
I'm going to assume that you accept the premise, but don't see how it proves the conclusion. If you actually don't get the premise either, you'll have to read the proofs ("it has been shown..."), or just accept that since all computer programs are expressed as a finite-length string of bits, those bits can be interpreted as a finite integer.
Here's the proof.
Since we accept that all computer programs can be mapped to integers, it follows that every program that computes a number (a strict subset of all programs) is mapped to an integer. Construct a mapping which takes the number and maps it to the number of the smallest program that generates that number.
Done, by construction.
(I didn't say it was practical.)
Read the book. It's good and free.
-Billy
It means that there are so many of them, you can't make a numbered list that contains all of them, even if you had an infinitely long list.
The book explains this brilliantly and very simply, and it's free. Read it!
-Billy
Of course it will. This is a universal problem with ALL power generation and use. It can be reduced ONLY by increasing the efficiency.
Again, this is universal. There's no energy production system that's immune to it. Further, the amount of the increase is related to the amount of power produced, NOT the type of energy source.
-Billy
Radiation would turn the usual high temp-high pressure tubing into something with holes resembling swiss cheese in a few years, so some exotic materials need to be used - and replaced every now and again.
I'd like to say I know you're wrong, but I don't. It just doesn't sound right to my half-trained ears. Could you provide a reference to explain this? Feel free to make it a technical one; I'm not an expert, as I mentioned, but my degree is in chemical engineering (although I work as a programmer), so I can follow it.
The rest of your post seems equally suspicious to me, but the one part I'll speak up against is your comments about steam. There you definitely have no clue on what you're talking about. Simply because steam was used for transmission of power a while ago does NOT make it primitive; on the contrary, it makes it (relatively) mature. Because it's so widely used, its properties have been very well explored, and efficiencies of systems using it are extremely high.
-Billy
Yes, it would be powerful if it were true. Warning: don't assume it's true just because you want it to be.
/could/ happen in highly hypothetical conditions; furthermore, their results were pretty useless to explain anything more complex than the most simple assemblies.)
Von Neumann established the neccessary complexity for an organism to be capable of evolution: it has to reproduce, self-diagnose, and self-repair. If it can't reproduce, it won't possibly evolve; if it can't self-repair, it won't have enough 'genetic' stability to evolve; and if it can't self-diagnose, it can't conserve energy by performing repairs only when needed. The size of these creatures suggests something below the previously known size threshold for these functions, which indicates a possibly lower complexity.
These might indeed show us a possible path to life as we know it, thus providing the first evidential path for abiogenesis. (The Miller experiments were fine, but only showed what
So I think a lot of people will be watching these. I certainly will -- but I'm not holding my breath, either.
-Billy
SPARK's assertions differ from C's because SPARK's are gueranteed to be complete and correct, otherwise the verifier won't let you past.
You could, in theory, use to do design by contract, but you'd have to be very careful to put your assertions in the right places, make sure that none of them have side effects, and manually do a few other things that a DbC language automatically takes care of for you. It'd be risky, but it's possible. It becomes MUCH harder when you add object orientation, though; managing inheritance of invariants becomes very difficult.
-Billy
Your point that "correctness isn't always necessary" is well taken. The more you need the more you have to pay, and not every project can afford the price.
The rest of your post absolutely requires the absence of a tool like SPARK. Throw SPARK into the mix, and all your grounding assumptions are absolutely wrong -- the specifications _do_ describe the interfaces, and the interfaces _do_ work together, and the code _does_ implement the specifications, and there are no possible exceptions.
Trivial examples all show the benifits of whatever new language feature has been added. It's really only after significant use and experience that we can judge how good something is in a large scale appplication.
So tell me -- how long has SPARK been around? How many projects has it been used in? With what level of success?
Are you judging it without knowledge?
I remember getting excited about the "Z specification" language in 1986, but in the end it was just too damn
hard for everyone. The programs were absolutely correct but if you wanted to change something later, you were back to square one. Forget about anything large involving multiple people.
I've seen it used too. And I agree.
I find SPARK different -- rather than a mathematical expression of operation, it allows you to build a mathematical specification (which is easier), and tie it provably to a computation (which is fun). It's still not easy, but it's easier.
Give me a sandbox, lego bricks, and let me play.. go away I don't like your rules.
No problem. I don't like embedded programming; some people do.
-Billy
So that fact that Ada had DoD funding for a denotational semantic specification and Java does not does have such a specification does not make Ada more portable and reliable (in the sense that a piece of code will produce the same result on different platforms).
You're right that the phrase "formal specification" was a bad choice on my part. Ada doesn't have an official formal specification (although SPARK does); what Ada has is a highly formal official specification, automatically verified by an extensive validation suite that every compiler must pass.
This official requirement made writing Ada compilers VERY hard (a big reason why Ada wasn't successful), but it also makes it possible to write unambiguous formal semantics for a clean, useful subset of Ada. This is what SPARK uses.
And SPARK does formally guarantee precisely what you claim it can't: that a piece of code will produce the same result on different platforms, and even on different compilers. Once you've verified that the code is valid SPARK, you also know that it's valid Ada, and that it's totally and purely portable. No annotations or theorem proving needed.
Choosing Ada as the basis for anything guarantees that few people will use it.
That's easy to say, but there's no choice here. It was Ada, an ad-hoc language, or no solution at all. Put that way, the choice is extremely simple.
I would argue with your statement on other facets, but you've left it ambiguous enough that you could claim it's correct no matter what the facts are. (All you have to do is say, "That's not what I meant by "few people.") Let me just say that SPARK appears to be the only product in its solution domain -- that is, there's no choice if you need to be 100% certain that your code won't throw an exception and give you an Arianne 5.
The module paradigm for languages (used by Ada and Modula-2)
Stop right there. Ada doesn't use "the module paradigm". It's a full-power object oriented standard, and has been since Ada 95. It's had genericity and static polymorphism since the original Ada.
Finally, just because you have a specification and code that exactly implements this specification does not mean that the application will not result in unintended results (e.g., the death of users or others).
There's no doubt of that. Or those results may have been the INTENDED results (military applications) -- the compiler can't tell the difference.
So I have to agree with you.
Frequently the problems encountered with software are a result of conditions that the designers did not forsee. That is, things that were not defined in the specification.
But using SPARK does mean that you DON'T have "problems encountered with software." If you have a problem, you know good and well where it came from -- bad specifications, not bad software. That's a huge improvement, wouldn't you agree? Narrowing down the location of the fault is the first step toward fixing it.
-Billy
Er... Read my message again. I wasn't knocking Eiffel; on the contrary, I was giving Bertrand credit for having DBC nailed before SPARK came along.
I also wasn't talking about Eiffel's support for DBC; I was describing DBC in general, or more accurately DBC without OO support. I didn't claim that OO isn't possible with DBC (on the contrary, I stated that it was, and I would explain it if asked). I didn't claim that Eiffel didn't have OO.
And finally, the huge thing that's new in SPARK that isn't in Eiffel is static contract checking. That's not present in Eiffel, for all its wonderful features.
-Billy
It's not a waste of time to describe what a function does. It's essential to keep "what" a function does distinct from "how" it does it. That's the whole point of interface versus implementation.
Consider a function with the following contract:Now, can you see how that's useful? And do you see that this tells you something _completely_ different than what you'd know if you read the actual source code for that function (perhaps an implementation of Newton's method)?
In the second case, your specification does not cover every aspect, which introduces loopholes, defeating the purpose of the contract.
That's what SPARK's automatic verifier is for -- to prove that there are no loopholes.
-Billy
Two statements there.
:-). Odd.
I would have been interested if all this instrumentation had been grafted onto a language like Java, or C++. But to have to switch to Ada just to be able to add in instrumentation that helps in code analysis?
Switching languages is a tiny effort compared to the change required to design your code for static validation. The SPARK people strongly recommend against trying to "switch" to SPARK; if you want the benefits, you have to code with it from the start. It's kind of like taking a 100,000 line C program written by 30 programmers over 10 years and trying to "switch" it to C++ -- it's theoretically possible, but in practice it's easier to start over.
And what they did in Ada would have been impossible in C++. It's significant that SPARK code will run EXACTLY the same on all compliant Ada compilers. No platform dependancies, no ambiguities, no undefined behavior... ALWAYS the same. You simply can't possibly define a subset of C++ which would be able to make those promises. I don't know if it would be possible with Java; since there's no formal specification of Java, probably not.
It's also funny that he WOW's at the idea of no dynamic memory allocation...
I felt that way too
The reason they did it is simple, though -- they wanted to be able to set absolute bounds on when a SPARK program will or will not fail (throw an exception). There's no way to do that with dynamic memory allocation as it's defined in Ada and most other languages.
Yes, that's limiting; no argument. But for some problems, particularly ones solvable by programs managing their own memory, the limitation doesn't matter compared to the benefits -- a SPARK program can execute without any runtime support code.
Why not just use a type safe language?
No such thing -- type safety is an uncomputable problem.
If you meant strongly typed, that's easy; Ada was already strongly typed. SPARK just guerantees that the programs will always run the same, and SPARK's verifier guarantees that the types are chosen and described correctly.
-Billy
Design By Contract was not invented by SPARK; the name was popularised by Bertrand Meyer, who added it to his "Eiffel" language.
:-).
/anything/ about how sqrt is computed, you can use it in powerful ways. Preconditions and postconditions can't always be as informative as the ones above are (the ones above define everything about the integer sqrt function), but they can give useful information.
Anyhow, DBC is totally distinct from object orientation. In DBC, each component in your software comes with a "contract" that states "if I am called when the _preconditions_ are true, I promise that after I run the _postconditions_ will be true."
The preconditions and postconditions are a group of logical statements, hopefully ones which are useful to your program
Let me give a little example.
function: sqrt( x )
preconditions:
- integer (x)
- positive (x)
postconditions:
- result > 0
- result * result x
Do you see what's happening there? Without knowing
Adding in object orientation support to DBC is a little more complex, but I won't go into that unless asked.
Traditional DBC systems, including Eiffel, couldn't verify your contracts, so most of them would translate the contracts into code, and include that code in the executable; if a contract failed, the code would throw an exception or otherwise fail. SPARK is interesting because it can detect contract failures without running the code; it can also detect when your contracts fail to promise enough.
-Billy
Patenting itself doesn't break the GPL. Patents without freely available licenses would do so, though.
IBM, for example, is talking about opposing software patents. They could set a shining example -- put their money where their mouth is -- by taking a first step and licensing some of their software patents for unrestricted use under the GPL.
Such a patent license would definitely meet the demands of the GPL; in fact, it would do the same thing to patent law that the GPL does to copyright law.
-Billy
I wonder how all the peace mongers would react if Hitler (the original, not some barely literate moron with a Texan accent) was alive today. You'd probably just let him be (unless he was American or Israeli.)
Don't spend too much energy wondering -- just read history to find a confirmation of your suspicions. The overwhelming sentiment in America before Pearl Harbor was antiwar; Americans saw Hitler as just another cruel, powerhungry dictator on a landmass full of cruel, powerhungry dictators. They weren't interested in entering yet another expensive war to help a group of nations that were still engaged in avoiding repayment for WWI debts. Charles Lindbergh wrote in this vein; his work is interesting.
He changed after Pearl Harbor, though. Almost the entire nation did.
-Billy
There are no tests that differentiate between heliocentric and geocentric either. It's purely a matter of notational convenience.
This seems to be a fundamental property of the universe, not a matter of missing knowledge. Any point in space and time can be selected as the origin, and all the equations will work out exactly the same. Moving points are different, but the differences don't allow you to establish preference for one point (the Sun) above another (the Earth).
For more info, google for Mach's Principle.
-Billy
Nope, that's the case; no Windows clients yet, and none in sight. It's possible that were one to be written, it wouldn't be very good at compatibility.
Use darcs instead if you care about cross-platform bitkeeper-like version control.
-Billy
What you really need is an engine that is connected only to a generator and always runs at a single speed and always the same loading.
That's a clever idea, but you'll pay more for it than you gain. Yes, your engine will be more efficient; but the overall system will generate more losses (or simply not be usable) because it can't get the output it needs from the engine. Remember, gas is still the most efficient source of power, even in a hybrid with regenerative braking. Storing energy in batteries, or converting from mechanical to electrical, wastes a LOT of energy (although it's better than throwing the energy away).
The Toyota has an interesting twist on this, though. Its engine obviously doesn't always run at the same speed and loading -- but it does always run at its optimal speed and loading. It does this by modifying its cylinder geometry on the fly. Essentially, if you only need half the power it only uses half of each cylinder. (Not to be confused with disabling cylinders -- all the cyclinders keep working; each one changes its power curve. Read more.
-Billy
A hierarchy is a /much/ weaker form of organization than a full graph. A DB filesystem would allow people to organize their files using a graph.
Organization would still be needed, though. Even the most powerful automatic categorizer and smart search tools won't save you from dumb organization.
-Billy
No, actually it's the result of a thorough understanding of arch as a result of comparing it with a LOT of other SCM systems. But you can get the same result as me by reading the arch manual, which discusses creating a new archive. Note that creating a new archive is distinct from creating a new workspace; a workspace has to be associated with an archive.
In other systems, including BitKeeper and darcs, creating a new workspace is the same thing as creating a new archive. They are truly distributed; there's no need to tell it which archive it'll be using, because the answer is "the one I'm working in right now". Every workspace is its own archive, every archive is its own workspace.
The difference is astounding -- it's like the difference between CVS and arch. And yes, I was an arch fan, I even converted someone else to arch. He uses darcs now, just like myself.
-Billy
SVN also compares poorly to BitKeeper and its kin. The problem is that SVN, like CVS, needs to have a configured central repository; BK doesn't.
There are some good free software alternatives; the only one I know of that works like BitKeeper is darcs. (Arch is very close, but it still requires you to configure a central archive.)
-Billy
Can you compare it to darcs? (I can't, because I've done some work on darcs and am not willing to pay money just to do a simple comparison.) I ask because the way you describe BitKeeper sounds pretty much like darcs.
(Except for the graphical utilities -- I'm told that darcs has an experimental graphical merge, but that's all right now.)
-Billy
I suspect others will comment on this too, but there are other close equivalents in the free software world.
Arch is groundbreaking, but it was designed in a rather ad-hoc way, and it _really_ shows. You have to know a lot about the implementation details in order to get stuff done in it.
Darcs is much, much easier to use, and is supported on more platforms (including win32). The shortcomings include slow execution time (due to a complex merging algorithm that's part of the reason it's much easier to use) and an unusual implementation language (I like Haskell, but I recognise that many people don't know it).
OpenCM and Monotone are in much earlier stages of development, and I haven't tried to use either in a production environment.
Bitkeeper still has one big advantage: it's got killer graphical utilities and it's really complete. Both arch and darcs are still growing into their full statures.
But I strongly recommend darcs. I don't see any reason to use any other SCM tool, honestly -- darcs _just works_ and is free. Copy the executables into your path, type 'darcs inittree', and start working; it's just that easy. No worries about file identities, no worries about archive locations; it's all taken care of thanks to a well-thought-out model.
-Billy
Regression tests are also useful _with_ a bug report -- they're a formal reproduction of the reported bug, and once you narrow down the cause they're also a proof of the accuracy of your judgement.
Actually, though, I use them mainly as what I call progression tests. Whenever I think of a feature or design point, I try to express it as a simple test. Then I add to my software code to pass that test. Tests don't hinder my work anymore; they help it along. Rather than the phycological disappointment of doing _additional_ work writing tests only to have my already-written software proven incomplete, I get the psychological reward of having my already written tests tell me when my work is done.
My point: regression tests help on many parts of the software life-cycle, if you use 'em.
-Billy
I always thought it was because they undercut the local competition and strong-armed their suppliers.
I don't have to deny that (and in many cases I can't; it's obvious historical fact). Strongarming suppliers DOES give Walmart a minor advantage, so it makes sense that they've used it. But that doesn't change the fact that they HAVE used inventory control more efficiently than any of their competitors, and that this efficiency translated into lower prices and produced their overpowering dominance. Without the efficiency, they would have NO dominance, and thus no ability to "strongarm" suppliers.
-Billy