cool article, interesting quote

David Parnas did some nice work about tabular specifications for control systems based on a Canadian nuclear power plant control system, and farther back, the NRL verification of the A-7 avionics code. One of his premises is that domain experts have to verify the specifications, and this means inventing a formalism that domain experts can pick up quickly yet is formal enough for the subsequent design and verification cycles.

More CS-oriented spec formalizations include UML diagrams and statecharts.

Parnas is a controversial guy, but I've always found him to be pretty much on the ball. I was at a conference once where at the keynote address he explained to a room full of formal verification people why computer science PhDs are useless on real world projects.

Sounds like the old gnu superoptimizer program. It really does generate every possible opcode sequence for a function; tests the sequence; and keeps the shortest/fastest sequence.

Kelly

Reply to
Kelly Hall
Loading thread data ...

You do have a fine sense of humour, I felt I should acknowledge that!

Dimiter

Ken Smith wrote:

Reply to
Didi

In article , Isaac Bosompem writes

Personally I thin they should teach intelligent design and creationism.....

There is only one Darwin and theory of evolution There is only one big ban theory (though note that neither address what existed before the big bang and what caused it AFAIK so they may not contradict some creationist theories)

However..... :-) There are several thousand religions all with their own creationists story. SO if you want to teach intelligent design and creationism do so but teach ALL of them equally....... :-) that should cause some interesting discussions in the right wing religious US ;-)

OK stick to the top 10 to start with..... :-) that will cause some fun when the Christians and Moslems realise that they start from same point :-)

I think David Ike and the Lizards should also have equal billing..... Otherwise teach science in science class and religion in religious classes.

--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England     /\/\/\/\/
/\/\/ chris@phaedsys.org      www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/
Reply to
Chris Hills

This is correct.... ALL navigators knew the earth was round and exactly how bit it was round the equator. The problem was actually navigating because there were no accurate clocks to fix the time and hence fix the longitude.

About 500 BC I think.

Not so. Columbus knew the exact equatorial size of the globe very well. They also knew the size land mass from Japan to Canaries reasonably accurately. What the educated man knew and what he said in public or in front of a priest was VERY different.

They also knew from trips round Iceland, Greenland and Canada where N America was. According to the Vikings they knew where and some S. American legends they knew where S. America was.

The problem was the Church (RC/Pope etc) The earth was flat heaven above hell below and the sun went round the earth (as did the moon). TO say any different was hearsay and would get you burnt at the stake.

The Pope had divided up the world going west between Portugal and Spain. there were lots of riches to be won and a LOT of politics.

If you read the history Columbus disappears from court for 5 years before making his "epic" journey. He then had a map which showed the world a little smaller and took EXACTLY the right amount of supplies to make landfall where he did.....

There is also the fact that his log book is inaccurate as he put his land fall in above the line and in the domain of Spain rather than below the line and in the domain of Portugal... After that possession was

9/10th of the law :-)

So the public 40% smaller was only there for the less well educated and as a smoke screen to hide the fact that Columbus knew there was a huge land mass out there with lots of commercial opportunities

It took 6 weeks to cross the Atlantic.... So where was he for the missing 5 years before first coming to court with the idea and actually publicly setting sale with exactly the right ships and provisions for the trip?

--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England     /\/\/\/\/
/\/\/ chris@phaedsys.org      www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/
Reply to
Chris Hills

Hardly.... ADa for 8051, PIC, AVR, HC08 etc

--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England     /\/\/\/\/
/\/\/ chris@phaedsys.org      www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/
Reply to
Chris Hills

In article , John Larkin writes

As I recall when Ada was produced they did a test suite and certification system for it at the same time. So when people started to write Ada compilers there was already a system in place. This has not been the case for other languages.

However "certified" as having passed the test suit and being "proven" are probably two different things. Besides you can still write bad code in any language.

The other minor problem I have seen is: in "safe" languages the programmer "knows" that if it compiles it is safe/good code...... leading to all sorts of problems.

--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England     /\/\/\/\/
/\/\/ chris@phaedsys.org      www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/
Reply to
Chris Hills

"[..]

However "certified" as having passed the test suit and being "proven" are probably two different things."

Correct.

" Besides you can still write bad code in any language.

[..]"

Correct.

Reply to
Colin Paul Gloster

When I was still studying (1979), a Master's thesis was awarded for a formal proof of a program in Pascal that was a Pascal pretty-printer. I forget the size, it might have been 1500 lines of code, but it was an entire year's hard work to formally prove it.

When the program was fed itself (the binary executable) as input, it dumped core. So much for correctness proofs!

It turned out that the lexical analyser used a "case" statement over the character being processed, and the Pascal runtime used the character as an index into a jump table of 256 members. Only trouble was, it used a signed character, so the 8-bit characters indexed backwards off the start of the jump table into random garbage, which became the next program counter.

True story, and the subject is still teaching CS, AFAIK.

The problem with C (and I speak as a professional software engineer who I humbly believe deserves the title, and has used C and C++ for preference in my own work for >25 years), is that it provides very little defense against non-local effects. If you run off the end of an array, you change something that wasn't part of the array. The array was part of your local concern, the other thing wasn't. And so on, examples abound. It isn't that hard to overcome most of the weaknesses with discipline, but a programming language that's to be used by the masses should make a better attempt to pander to the laziness of the masses. C# and Java are only marginally better... At least with assembly you *know* you're handling a loaded gun, and if you get something wrong the consequences are obvious.

Add to that the culture of ignoring error returns, returning error codes but not what object was the subject of the error, etc, and you engender a "hopeful" programming style - vis the Posix API for example. Try to open a file, and get an error "No such file or directory". Well was it a file or a directory that was missing? Which one? The kernel knows, but has no way to report it - absolutely hopeless. Every error that is detected must be reported *along with the maximum detail* that can be added to what might have already been reported by an called routine... The entire recovery chain must account for every extra level of detail or consequence, allowing the program to explicitly clear error conditions on recovery but defaulting to propagating them to the point of stopping the program. Note it's *hard* to do this properly with exceptions, and I've never seen a program that does. Anyhow... show me the language that has intrinsic support for managing such error cascades... I don't believe there is one. We use a system I built in C++ that does it, and it's really alarmingly easy to incorporate into a development environment and culture. I can't understand why such systems aren't more widespread.

These two things alone (non-local effects and bad error management) account for 99% of the unreliability of Windows and Windows apps. The other 1% might mostly be true logic errors, but... "Unknown error 0x8000000" indeed! Who hasn't seen that one? It's an absolute disgrace, yet can occur in nearly every Windows app.

Clifford Heath.

Reply to
Clifford Heath
[...]

I don't know about the others, but -- why not ?

--
http://www.flexusergroup.com/
Reply to
Bjarne Bäckström

He didn't take along enough provisions to make it to India. That means he either believed the planet was a lot smaller or thought he was going to find someplace else before he got half way there.

He died believing he'd made it to the East Indies.

--
Grant Edwards                   grante             Yow!  Hey, LOOK!! A pair of
                                  at               SIZE 9 CAPRI PANTS!! They
                               visi.com            probably belong to SAMMY
                                                   DAVIS, JR.!!
Reply to
Grant Edwards

so do I, "abstraction = avoidance" is true only because the abstractions are poorly implemented, not because the concept is wrong, abstraction is the only path to increased productivity, in every field not just software, when I cut a piece of wood with a powered tablesaw I don't care how the tablesaw's motor armature works or how it was put together, I just buy it and use it and leave the motor abstraction to someone else more qualified.

Currently, in the software field, everyone is still in the basement homebrewing their own motor armatures and we are all hacks at it (with C and C++ being the basement machine shop), no wonder the end product is so expensive, time consuming and looks all crooked.

Reply to
steve

He knew the EXACT size of the globe around the equator. He also knew the size of the land mass from Japan to the Canaries.

So he knew how big the gap between Japan and Spain was going west from Spain. Yet he only took enough provisions to cross the Atlantic....

SO he was either very stupid or he did not want to publicise a whole new commercial opportunity until they knew what they were getting into. this is what he was doing for 5 years when he "disappeared" from court before setting off on his public journey of discovery.

--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England     /\/\/\/\/
/\/\/ chris@phaedsys.org      www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/
Reply to
Chris Hills

Ooops...typo. You wrote "big" were you obviously meant "little". ;)

-Le Chaud Lapin-

Reply to
Le Chaud Lapin

... snip ...

Something is very wrong here. Pascal's characters are not signed, in fact they are not even integers. They can be put into one-to-one correspondence with some integers by the ord function, and the result is not portable. However it is handy in developing text to number translations. So a case statement would be of the form:

CASE ch OF 'a': athings; 'b', 'c', 'd', 'e', 'f': bthings; END;

and anything other than 'a'..'f' should cause a trap.

--
"If you want to post a followup via groups.google.com, don't use
 the broken "Reply" link at the bottom of the article.  Click on 
 "show options" at the top of the article, then click on the 
 "Reply" at the bottom of the article headers." - Keith Thompson
More details at: 
Also see
Reply to
CBFalconer

We do this in hardware verification all the time. The "architecture model" is the basis for comparison. Often (particularly at the beginning of a project) a flaw is found in it by the simulation model. Then there are drivers and monitors to check for proper operation of the simulation model. Formal verification is also used to "prove" exactness between models.

1M monkeys?
--
  Keith
Reply to
Keith

I don't know much about many things but it seems to me that all that has happened is that people have built layers of abstraction upon more layers of abstraction upon...... and so on.

I don't really know what abstraction is but I would assume that if you wanted to use it then you would have to 'assume' that the layer of abstraction you are building your layer of abstraction upon makes sense, you understand it and it 'works'

But, it seems that the reason for introducing another layer of abstraction is to try and hide a 'confusing' or otherwise 'broken' bit in the layer of abstraction beneath the new one. And then you get the opportunity to add some other abstract thing to your new layer.

It seems strange to me, because I don't know about this stuff, but what is the point of your new layer of abstraction if it is built upon a layer of abstraction that used the 'bing' language and you call it 'bong'?

Seems to me that you have just abstracted bing. If bing was shit to begin with then can you be so sure that bong is better?

There was something about this sort of thing in the blibble

DNA

Reply to
Genome

I have used Ada extensively for the last 15 years in embedded systems. It has a lot of advantages but can be abused as well. I still consider it the best choice for safety critical applications, especially for large, long life applications because even bad Ada (and I've seen plenty) is easier to develop and maintain in these type of uses. The compilers are quite good and find many of the common errors poor programmers make and the encapsulation of common resources into packages with separate specifications and implementations make development and understanding easier and more manageable within the development team.

I also use Ada for a lot of PC GUI-based simulators and find it a great choice for these as well.

By the way, the new website for the Ada community is

formatting link
(or
formatting link
as well).

--

------------------------------------------------------------------------

-- Jerry Petrey

--

-- NOTE: please perform appendectomy on email address before replying

------------------------------------------------------------------------

Reply to
Jerry Petrey

I think the problem is the scriptkiddies they're cranking out of the diploma mills - they never learn to actually design a program - they sit down and start entering their program before they've even written it. I first read about this phenomenon when they were talking about teaching everybody BASIC, which even I'll agree, is a crappy language.

The secret is to design it before you write a single line of code. Of course, having ~20 yrs. experience helps. :-)

Cheers! Rich

Reply to
Rich Grise

It seems to be worse than that. Either they pay someone to write it for them or the one geek in the study group writes for everyone.

Reply to
Jim Stewart

Ahh, yes, but what 'true' c++ programmer would want to write a subsystem that is not "technically correct" but just does what it has to do, the simplest and most efficient way? The answer is the c++ programmers that now use java and c#, or the programmers that created java and c++.

I find that the biggest problem with a hardcore c++ programmer is that they have no commercial programming sense.

Reply to
The Real Andy

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.