|
Size: 281
Comment:
|
← Revision 3 as of 2006-08-22 14:09:09 ⇥
Size: 676
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