Expressing and Verifying Business Contracts with Abductive Logic Programming

摘要

In this article, we propose to adopt the SCIFF language to specifyudbusiness contracts and show how its proof procedure is useful toudverify contract execution and fulfilment. SCIFF is a declarativeudlanguage based on abductive logic programming, which accommodatesudforward rules, predicate definitions, and constraints over finiteuddomain variables. Its declarative semantics is abductive, and can beudrelated to that of deontic operators; its operational specification isuda sound and complete proof procedure, defined as a set of transitionudrules, which has been implemented and integrated into a reasoning andudverification tool. A variation of the SCIFF proof-procedure (g-SCIFF)udcan be used for static verification of contract properties.ududWe demonstrate the use of the SCIFF language for business contractudspecification and verification, in a concrete scenario. In order toudaccommodate integration of SCIFF with architectures for businessudcontract, we also show the encoding of SCIFF contract rules in RuleML.