| 000 | 01005camuu2200289 a 4500 | |
| 001 | 000045340401 | |
| 005 | 20070413134449 | |
| 008 | 921230r20061992enk b 001 0 eng | |
| 010 | ▼a 92253188 | |
| 020 | ▼a 0521417236 (hardback) | |
| 020 | ▼a 9780521417235 (hardback) | |
| 020 | ▼a 0521032512 (paperback) | |
| 020 | ▼a 9780521032513 (paperback) | |
| 035 | ▼a (KERIS)REF000006693430 | |
| 040 | ▼a DLC ▼c DLC ▼d DLC ▼d 211009 | |
| 050 | 0 0 | ▼a QA76.615 ▼b .P33 1992 |
| 082 | 0 0 | ▼a 005.13/1 ▼2 22 |
| 090 | ▼a 005.131 ▼b P123d | |
| 100 | 1 | ▼a Padawitz, Peter , ▼d 1953-. |
| 245 | 1 0 | ▼a Deduction and declarative programming / ▼c Peter Padawitz. |
| 260 | ▼a Cambridge ; ▼a New York : ▼b Cambridge University Press , ▼c 2006, c1992. | |
| 300 | ▼a vi, 279 p. ; ▼c 26 cm. | |
| 440 | 0 | ▼a Cambridge tracts in theoretical computer science ; ▼v 28 |
| 504 | ▼a Includes bibliographical references (p. [269]-274) and index. | |
| 650 | 0 | ▼a Declarative programming. |
| 945 | ▼a KINS |
소장정보
| No. | 소장처 | 청구기호 | 등록번호 | 도서상태 | 반납예정일 | 예약 | 서비스 |
|---|---|---|---|---|---|---|---|
| No. 1 | 소장처 과학도서관/Sci-Info(2층서고)/ | 청구기호 005.131 P123d | 등록번호 121144505 | 도서상태 대출가능 | 반납예정일 | 예약 | 서비스 |
컨텐츠정보
책소개
Declarative programs consist of mathematical functions and relations and are amenable to formal specification and verification, since the methods of logic and proof can be applied to the programs in a well-defined manner. Here Dr Padawitz emphasizes verification based on logical inference rules, i.e. deduction (in contrast with model-theoretic approaches, deductive methods can be automated to some extent). His treatment of the subject differs from others in that he tries to capture the actual styles and applications of programming; neither too general with respect to the underlying logic, nor too restrictive for the practice of programming. He generalizes and unifies results from classical theorem-proving and term rewriting to provide proof methods tailored to declarative program synthesis and verification. Detailed examples accompany the development of the methods, whose use is supported by a documented prototyping system. The book can be used for graduate courses or as a reference for researchers in formal methods, theorem-proving and declarative languages.
The book can be used for graduate courses or as a reference for researchers in formal methods, theorem-proving and declarative languages.
정보제공 :
목차
Introduction; 1. Preliminaries; 2. Guards, generators and constructors; 3. Models and correctness; 4. Computing goal solutions; 5. Inductive expansion; 6. Directed expansion and reduction; 7. Implications of ground confluence; 8. Examples; 9. EXPANDER: inductive expansion in SML; References; Index.
정보제공 :