|
⇤ ← Revision 1 as of 2005-03-27 18:48:59
Size: 281
Comment:
|
Size: 668
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 3: | Line 3: |
| See: http://www.mimuw.edu.pl/~sl/teaching/PMW/SMV-doc/tutorial/node32.html | "Suppose that instead of specifying the exact function of the ALU in our abstract model, we simply use a symbol f to denote this function. Suppose further that we use the same function symbol in our implementation, and we are able to prove a refinement relation between the two. It would then follow that the refinement holds for any concrete function we might want to plug in place of f." - http://www.mimuw.edu.pl/~sl/teaching/PMW/SMV-doc/tutorial/node32.html |
UninterpretedFunctions are equivalent to Abstract Functions, but used in a theoretical framework. You can think of it as a function place holder because it is an undefined or "uninterpreted" function.
"Suppose that instead of specifying the exact function of the ALU in our abstract model, we simply use a symbol f to denote this function. Suppose further that we use the same function symbol in our implementation, and we are able to prove a refinement relation between the two. It would then follow that the refinement holds for any concrete function we might want to plug in place of f." - http://www.mimuw.edu.pl/~sl/teaching/PMW/SMV-doc/tutorial/node32.html