Soundness in verification of algebraic specifications with OBJ |
| |
| Authors: | K.O. Wilander |
| |
| Affiliation: | aDepartment of Mathematics, Uppsala University, P.O. Box 480, SE-751 06 Uppsala, Sweden |
| |
| Abstract: | The algebraic specification tools of the OBJ family have no notion of open terms or quantifiers. Nonetheless there are methods of proving universally quantified statements about specifications. These methods are examined and found to be unsound. |
| |
| Keywords: | Soundness OBJ Algebraic specification Verification Behavioural specification |
| 本文献已被 ScienceDirect 等数据库收录！ |
