Semantics and logic of object calculi
Proceedings - Symposium on Logic in Computer Science - Trang 113-122
Tóm tắt
The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic for the object calculus and to suggest possible extensions. For the purposes of this discussion we use an informal logic of predomains in order to avoid any commitment to a particular syntax of specification logic.
Từ khóa
#Logic programming #Calculus #Object oriented programming #Machinery #Object oriented modeling #Computer scienceTài liệu tham khảo
10.1007/3-540-45719-4_32
10.1007/3-540-45314-8_22
reus, 1999, A logic of recursive objects, Formal Techniques for Java Programs, 251, 58
reus, 1999, A logic of recursive objects (abstract), Lecture Notes in Computer Science, 1743, 107
10.1007/978-0-387-35358-6_26
10.1006/inco.2001.2927
america, 1999, A proof theory for a sequential version of POOL
10.1007/BFb0030634
abadi, 1996, A Theory of Objects, 10.1007/978-1-4419-8598-9
10.1006/inco.1996.0052
10.1109/52.300040
10.1145/286942.286973
10.1007/3-540-45315-6_9
calcagno, 2001, A logic for objects
o'hearn, 2001, Local reasoning about programs that alter data structures, LNCS, 2142, 1
leino, 1998, Recursive object types in a logic of object-oriented programs, Nordic Journal of Computing, 5, 330