What is the 'object specification logic' of Sernadas et al., presented in various papers ? It is a the application of multi-sorted first-order temporal logic to the specification and verification of multi-agent systems but with an immediate focus on the paradigm of object oriented programming. Or rather, it is parametrization of such logics indexed by agents (and combinations of agents) which cries out for a Jacobs-type fibred category approach. It is a multi-modal logic with operators representing 'next', 'previously', 'all time in the future (excluding the present)' , etc. It builds upon previous work in theoretical computer science and has a close connection to Joseph Goguen's category theoretic framework for software engineering and general systems theory. The semantics are based on the combination of individual (local) run-time histories, functions $\mathbb{N} \rightarrow P$ where $P$ is, roughly speaking, a space of sets of possible attributes and acts.
Recall how in UDIL $D_0$ represents a space of possible propositional meanings or just propositions in a extra-linguistic sense-oriented or semantic sense (think Fregean Gedanke or along the lines of Bolzano), quite like the Stoic lekta. Now what Sernadas et at. did was sneak in a space (a sort) of possible actions for a given agent $c$ (or rather 'class' in OOP speak, a template for actual agents). They call this sort $\tau_c$. Since their logic is a temporal modal logic they can have contingent equalities. That is $t_1 = t_2$ can be thought to hold at one time but not at another. But how do they specify that an agent is performing a certain 'act' now ? With a kind of 'indexical' constant (of sort $\tau_c$ !) represented by the unpleasant notation $occ$ (short for occurs). Thus for a given agent $c$ we could write $occ = says('hello')$ to express that $c$ (or rather an object in this class) is performing the action of saying hello at the present moment, where $says$ is given the signature $string \rightarrow \tau_c$.
No comments:
Post a Comment