Some Problems in Certifying Microprograms
| Autor: | Jr. George B. Leeman |
|---|---|
| Rok vydání: | 1975 |
| Předmět: |
Correctness
Programming language Abstract program computer.software_genre Theoretical Computer Science Commutative diagram Algebra Automated theorem proving Computational Theory and Mathematics Hardware and Architecture Microcode Hardware_CONTROLSTRUCTURESANDMICROPROGRAMMING computer Software Mathematics |
| Zdroj: | IEEE Transactions on Computers. :545-553 |
| ISSN: | 0018-9340 |
| DOI: | 10.1109/t-c.1975.224258 |
| Popis: | A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman [1]. However, the computer discussed has some realistic characteristics not shared by the machine treated in [1], and the details of the microcode validation are complicated by this fact. A formal technique for partitioning the proof is presented and illustrated with examples. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|