Electronic markets, dispute resolution and negotiation protocols are three types
of application domains that can be viewed as open agent societies. Key characteristics
of such societies are agent heterogeneity, conflicting individual goals and
unpredictable behaviour. Members of such societies may fail to, or even choose
not to, conform to the norms governing their interactions. It has been argued that
systems of this type should have a formal, declarative, verifiable, and meaningful
semantics. We present a theoretical and computational framework being developed
for the executable specification of open agent societies. We adopt an external
perspective and view societies as instances of normative systems. In this paper
we demonstrate how the framework can be applied to specifying and executing
a contract-net protocol. The specification is formalised in two action languages,
the C+ language and the Event Calculus, and executed using respective software
implementations, the Causal Calculator and the Society Visualiser. We evaluate
our executable specification in the light of the presented case study, discussing the
strengths and weaknesses of the employed action languages for the specification of
open agent societies.