Puccetti / Afford / Allam The Programming and Proof System ATES

Advanced Techniques Integration into Efficient Scientific Software
1991
ISBN: 978-3-642-84542-0
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 1, 280 Seiten, eBook

Reihe: Research Reports Esprit

Today, people use a large number of "systems" ranging in complexity from washing machines to international airline reservation systems. Computers are used in nearly all such systems: accuracy and security are becoming increasingly essential. The design of such computer systems should make use of development methods as systematic as those used in other engineering disciplines. A systematic development method must provide a way of writing specifications which are both precise and concise; it must also supply a way of relating design to specification. A concise specification can be achieved by restricting attention to what a system has to do: all considerations of implementation details are postponed. With computer systems, this is done by: 1) building an abstract model of the system -operations being specified by pre-and post-conditions; 2) defining languages by mapping program texts onto some collection of objects modelizing the concepts of the system to be dealt with, whose meaning is understood; 3) defining complex data objects in terms of abstractions known from mathematics. This last topic, the use of abstract data types, pervades all work on specifications and is necessary in order to apply ideas to systems of significant complexity. The use of mathematics based notations is the best way to achieve precision. 1.1 ABSTRACT DATA TYPES, PROOF TECHNIQUES From a practical point of view, a solution to these three problems consists to introduce abstract data types in the programming languages, and to consider formal proof methods.

Zielgruppe

Research

Autoren/Hrsg.

Afford, Max

Puccetti, Armand

Allam, Rafat

Weitere Mitwirkende

Brocard, D.

Gagert, P.

Gribomont, P.

Pirotte, O.

Pucetti, A.

Raguideau, J.

Remouchamps, A.

Ten Cate, E.

Inhaltsverzeichnis

1 Introduction.- 1.1 Abstract data types, Proof techniques.- 1.2 Motivation.- 1.3 Organization of the book.- 1.4 Acknowledgements.- 2 State of the Art.- 2.1 Abstract specification and programming languages.- 2.2 Proof systems.- 2.3 Conclusions.- 2.4 References.- 3 The Programming Language.- 3.1 General presentation.- 3.2 Types and operators.- 3.3 Constructions and algorithms.- 3.4 Structures and modules.- 3.5 Development with ATES.- 3.6 Advanced features.- 4 The Applications within the ATES Project.- 4.1 Introduction.- 4.2 The first application.- 4.3 The second application.- 4.4 Performance considerations.- 4.5 References.- 5 The Specification and Proof Language.- 5.1 Basic mathematical elements for proof.- 5.2 Axioms.- 5.3 Types and Operator specifications.- 5.4 Proof elements.- 6 Proving the Correctness of ATES Programs.- 6.1 Definition of the correctness.- 6.2 The interactive proof environment.- 6.3 Proving the verification conditions.- 6.4 Example: the 1D heat transfer problem.- 6.5 Conclusions.- 6.6 References.- 7 Extending the Techniques to Parallel Programs.- 7.1 Formal synthesis and verification of concurrent programs.- 7.2 Validation of the approach in the real-time area.- 7.3 References.- 8 Implementation Issues.- 8.1 Generalities.- 8.2 The ATES compiler.- 8.3 The ATES proof system.- 8.4 The ATES correctness proof system.- 8.5 References.- 9 Conclusion.- Appendix A. Formal Specification of the 1D Heat Transfer Problem.- Appendix B. Grammar of the ATES Specification Language.- Appendix C. Grammar of the ATES Source Language.

Leseproben

2
Blackburn halted a few paces away from the dead man and passed a handkerchief across his dewed face. "Can you turn off this confounded heat?" he murmured. "Place is like a Turkish bath." And as Pimlott started away, he added quickly: "Get everybody outside, too. And close those front doors." Jeffery turned and looked about the building. There were four windows, glassless but fitted with heavy iron shutters which opened outward. These apertures, set breast high, showed the thickness of the massive walls, for the sills were almost a yard wide. A cough by his side made him wheel. Mr. Pimlott stood there, transferring a pellet of chewing-gum to his mouth. "This," he announced owlishly, "is a strange business." "True—very true," Jeffery agreed thoughtfully. His eyes had strayed past his companion to the carpet slippers which enclosed the feet of the dead man. Pimlott saw the significance of the glance and gave a dry snigger. "You haven't seen anything yet?" he said. "Just come round here a moment." Without waiting for assent, he led the way to the side of the altar. Jeffery, with a final frowning stare at the slippers, followed him. Pimlott halted suddenly and shot out a forefinger. "Look there!" A white tablecloth had been laid on the floor. On it three plates were placed. The first contained slices of cooked ham, the second an uncut loaf of white bread, and the third a slice of angel cake with cream filling, writhing in elaborate scrolls about the top. Anything more incongruous in these surroundings could scarcely be imagined. "A picnic," commented Blackburn grimly. "It was for a dead man, then!" Pimlott looked very wise. "Angel cake was a favourite of Mr. Roger's. He was a baby for sweets!" He dropped his eyes and masticated violently. "But what's it doing down here?" "I'll ask you one," Jeffery countered. "How did Roger Rochester walk across that mud-patch outside without leaving traces of clay on his slippers. And if he didn't walk across the mud, whose tracks are those we saw outside?" "But Roger couldn't have got in here that way," the other objected. "The door was locked! I saw Prater use a key to open it." He paused and added brightly: "Besides, one of those tracks in the mud leads away from this chapel. And that one certainly doesn't belong to Roger!" Jeffery poked a cigarette into his mouth and struck a match so viciously that it broke. "Mad," he said. "Mad! It all boils down to one thing!" Trevor Pimlott, eyes wide behind his glasses, whispered: "Witchcraft? Oh, I say!" "Why not?" Jeffery swung round on him. "Murderer rubs himself with stolen unguent and materializes out of thin air!" He broke off with a dry chuckle. "Lord! I'll talk myself into believing it if I go on like this! Come on—let's get back to fundamentals. We've got a corpse, haven't we? Let's get back to a sane and matter-of-fact beginning! A man's been killed! Right!" "And we're not even sure whether it is murder," the private detective pointed out. "People have committed suicide by stabbing themselves, you know." Blackburn did not answer. They walked back to where Dr. Austin was rising to his feet. He turned to face them. "Not much to report," he said. "Fairly straight-out killing. Powerful knife thrust through the left breast, the weapon taking a slightly upward tilt before lodging in the major blood-vessels about the heart. Broad blade of knife inflicted wide slitting wound—accounts for amount of blood shed. Thrust sudden and wielded by a strong arm." "Suicide?" Austin shook his head slowly. "Can't say without an autopsy. But I don't think so. The thrust is too strong, too deep, for voluntary infliction." Jeffery nodded. "What about the time of death?" "Roughly twelve hours ago. Can't Say nearer than that." Mr. Pimlott was clearly disappointed. "You can't?" Austin shook his head. Jeffery nodded, his eyes on the body all his feet. "Could you say if Rochester was standing on this spot when he was struck down?" "Either on this spot or somewhere very near it." "How do you know?" demanded Pimlott. "Merely common sense," Austin said sharply. "When the blood-vessels of the heart are penetrated, the haemorrhage begins at once. There's no sign of blood anywhere else in this place. Again, you'll notice that there's no trace of blood beneath the body, which seems to prove he must have dropped almost immediately, even before the blood had time to drip from the wound to the floor." "Of course." Blackburn smoked in silence for a moment. "You say, Doctor, that this knife-thrust had great strength behind it?" "Extraordinary strength, really. The knife-blade has penetrated the heart." "Then I take it that it would have been impossible for a woman to have inflicted the wound?" Austin was wary. "Unless she was an extraordinarily powerful woman." Jeffery was silent for a moment. Then, turning abruptly, he walked to the closed doors of the chapel and, turning, addressed the young doctor sharply: "Would it be possible to inflict that wound by throwing the knife from a point beyond these doors?" "Almost impossible." The reply came without hesitation. "Not only would the thrower have to be an expert marksman to find the heart at such a distance, but he would need strong light to make such a hit. Again, the weapon is buried too deeply to have lodged in the body by means of throwing." Austin shook his head. "No, Mr. Blackburn. From the cursory examination given the body, I should say that the person who thrust that knife stood directly in front of Roger, wielding the stroke with every atom of his strength." He paused and nodded to Jeffery. "Come here." When the three men stood over the body, Austin pointed down. "See for yourself. Not only has the knife penetrated directly to the hilt, but also the haft has impressed itself into the clothing. The knife has been thrust into the body as far as it could go. And that takes a powerful arm!" He considered moodily. "It's going to take all my strength, to get that knife out of the wound." "That's going to be a messy business," Blackburn agreed. "I think we can leave that in your hands." "And use a handkerchief," chimed in Pimlott. "You know—finger-prints." Brian said coldly: "Of course." He stooped over the body and Jeffery turned away. Almost a minute passed before the doctor rose and placed the knife on the altar. Blackburn moved across and examined it. The broad blade, tapering to a point and keen as a razor at the edges, was fitted into a wooden handle, a handle grooved into shallow undulations. He replaced it on the altar and turned back to Pimlott. "Would you cover the body with that cloth? It's nudity rather disturbs me." "Just a moment." Austin stayed Pimlott with a gesture. He spoke to Jeffery. "There's one small detail you ought to know. It may have nothing to do with this murder—but, all the same..." His voice trailed away and he bent over the body, lifting the right arm stiffly. "Take a look at the underside of the wrist." Both men did so. "It's only a scar," exclaimed Pimlott. Jeffery was running his fingers over the half-healed cicatrix. He noticed that the skin on either side was red and inflamed. "Septic, I should say, Doctor. About how old would it be?" "About a month old." Pimlott was regarding the mark, head on one side. "I say," he said abruptly, "there's more in this than meets the eye, you know." "Indeed?" "Yes!" The little man's tone was defensive. "I'd like to know just how Mr. Rochester got that scar on his wrist. I mean—he wasn't the kind of man who ever did any manual labour. I can't see how he could have cut himself by accident. And it's such an extraordinary place to be wounded—on the inside of the wrist! If the cut was made by design, well, what does it mean?" Brian Austin nodded. "I see the point of our friend's argument. Roger was an old woman about knives and firearms. I remember showing him a case of scalpels I have in my medical kit and he went quite white at the sight of them. And I can't imagine him cutting himself without running to someone for comfort. In that case, he'd most likely come to me. Yet this is the first indication I've had of this wound." Blackburn was pulling thoughtfully at his lower lip. He shook his head slowly. "I can see," he said grimly, "that the sooner I get the Department on to this business, the better. This is no task for a lone hand." He paused, to swing off at a tangent: "By the way, Doctor, what time did the rain begin down here last night?" Austin blinked a little at the rapid change of subject. He exchanged an inquiring glance with Pimlott, who was covering the body with the cloth. "About half past nine, I believe. I remember Roger pottering in and out of the drawing-room where we were sitting. Once he crossed to the...