| Autor: |
Brauer, W., Gries, D., Stoer, J., Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, von Wright, Joakim, Grundy, Jim, Harrison, John, Laibinis, Linas |
| Zdroj: |
Theorem Proving in Higher Order Logics (9783540615873); 1996, p315-330, 16p |
| Abstrakt: |
We describe an implementation of general (abstract) lattice theory in the HOL system and its use in transformational reasoning within concrete instances of lattices, using the window inference of HOL. The implementation is extensible; users can add new instances of lattices and all the existing transformation rules are then available for the added structures. As a particularly promising application we briefly describe how our system can be used as part of a tool for transformational reasoning about programs (program refinement). [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
