Skip to main content
SpringerLink
Log in

FCL: A Formal Language for Writing Contracts

  • Conference paper
  • First Online:
Quality Software Through Reuse and Integration (FMI 2016, IRI 2016 2016)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 561))

Abstract

A contract is an artifact that records an agreement made by the parties of the contract. Although contracts are considered to be legally binding and can be very complex, they are usually expressed in an informal language that does not have a precise semantics. As a result, it is often not clear what a contract is intended to say. This is particularly true for contracts, like financial derivatives, that express agreements that depend on certain things that can be observed over time such as actions taken of the parties, events that happen, and values (like a stock price) that fluctuate with respect to time. As the complexity of the world and human interaction grows, contracts are naturally becoming more complex. Continuing to write complex contracts in natural language is not sustainable if we want the contracts to be understandable and analyzable. A better approach is to write contracts in a formal language with a precise semantics. Contracts expressed in such a language have a mathematically precise meaning and can be manipulated by software. The formal language thus provides a basis for integrating formal methods into contracts. This paper outlines fcl, a formal language with a precise semantics for expressing general contracts that may depend on temporally based conditions. We present the syntax and semantics of fcl and give two detailed examples of contracts expressed in fcl. We also sketch a reasoning system for fcl. We argue that the language is more effective for writing and analyzing contracts than previously proposed formal contract languages.

This is a revised and extended version of [9]. This research was supported by NSERC.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Andersen, J., Elsborg, E., Henglein, F., Simonsen, J., Stefansen, C.: Compositional specification of commercial contracts. Int. J. Softw. Tools Technol. Transfer (STTT) 8(6), 485–516 (2006)

    Article  Google Scholar 

  2. Athan, T., Boley, H., Governatori, G., Palmirani, M., Paschke, A., Wyner, A.: OASIS LegalRuleML. In: Francesconi, E., Verheij, B. (eds.) ICAIL, pp. 3–12. ACM (2013)

    Google Scholar 

  3. Athan, T., Governatori, G., Palmirani, M., Paschke, A., Wyner, A.Z.: LegalRuleML: design principles and foundations. In: Faber, W., Pashke, A. (eds.) The 11th Reasoning Web Summer School, pp. 151–188. Springer, Germany, July 2015

    Google Scholar 

  4. Attorney, R.S.: Contracts: The Essential Business Desk Reference. Nolo (2010)

    Google Scholar 

  5. Bahr, P., Berthold, J., Elsman, M.: Certified symbolic management of financial multi-party contracts. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, 1-3 September 2015, pp. 315–327 (2015)

    Google Scholar 

  6. Blum, B.A.: Contracts: Examples and Explanations, 4th edn. Aspen Publishers, New York (2007)

    Google Scholar 

  7. Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda — a functional language with dependent types. In: TPHOLs, vol. 9, pp. 73–78. Springer (2009)

    Google Scholar 

  8. Farmer, W.M.: The seven virtues of simple type theory. J. Appl. Logic 6, 267–286 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  9. Farmer, W.M., Hu, Q.: A formal language for writing contracts. In: 2016 IEEE 17th International Conference on Information Reuse and Integration (IRI 2016), pp. 134–141. IEEE (2016)

    Google Scholar 

  10. Fenech, S., Pace, G.J., Schneider, G.: Automatic conflict detection on contracts. In: International Colloquium on Theoretical Aspects of Computing, pp. 200–214. Springer (2009)

    Google Scholar 

  11. Finan, M.B.: A discussion of financial economics in actuarial models: a preparation for exam MFE/3F (2015). Prepared for Arkansas Tech University

    Google Scholar 

  12. Goodchild, A., Herring, C., Milosevic, Z.: Business contracts for B2B. In: Proceedings of the CAISE00 Workshop on Infrastructure for Dynamic Business-to-Business Service Outsourcing, Stockholm, Sweden (2000)

    Google Scholar 

  13. Governatori, G., Milosevic, Z.: A formal analysis of a business contract language. Int. J. Coop. Inf. Syst. 15(04), 659–685 (2006)

    Article  Google Scholar 

  14. Governatori, G., Rotolo, A.: Logic of violations: a gentzen system for reasoning with contrary-to-duty obligations. Australas. J. Logic 4, 193–215 (2005)

    MathSciNet  MATH  Google Scholar 

  15. Hvitved, T., Klaedtke, F., Zălinescu, E.: A trace-based model for multiparty contracts. J. Logic Algebraic Program. 81, 72–98 (2012)

    Google Scholar 

  16. Linington, P.F., Milosevic, Z., Cole, J., Gibson, S., Kulkarni, S., Neal, S.: A unified behavioural model and a contract language for extended enterprise. Data Knowl. Eng. 51(1), 5–29 (2004)

    Article  Google Scholar 

  17. McNamara, P.: Deontic logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2014 (2014)

    Google Scholar 

  18. Norell, U.: Towards a Practical Programming Language based on Dependent Type Theory. Ph.D. thesis, Chalmers University of Technology (2007)

    Google Scholar 

  19. Norell, U.: Dependently typed programming in Agda. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI 2009, vol. 2, pp. 1–2. ACM, New York (2009)

    Google Scholar 

  20. Peyton Jones, S.L.: Composing contracts: an adventure in financial engineering. In: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science, vol. 2021, p. 435. Springer (2001)

    Google Scholar 

  21. Peyton Jones, S.L., Eber, J.M.: How to write a financial contract. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming. Cornerstones in Computing, pp. 105–130. Palgrave (2003)

    Google Scholar 

  22. Poole, J.: Textbook on Contract Law, 11th edn. Oxford University Press, Oxford (2012)

    Book  Google Scholar 

  23. Prisacariu, C., Schneider, G.: An algebraic structure for the action-based contract language cl-theoretical results. Technical report 361, Department of Informatics, University of Oslo, Oslo, Norway (2007)

    Google Scholar 

  24. Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 174–189. Springer (2007)

    Google Scholar 

  25. Prisacariu, C., Schneider, G.: Towards a formal definition of electronic contracts. Technical Report 348, Department of Informatics, University of Oslo, Oslo, Norway (2007)

    Google Scholar 

  26. Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Logic Algebraic Program. 81, 458–490 (2012)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

The authors are grateful to the reviewers for their comments and suggestions. This research was supported by NSERC.

Author information

Authors and Affiliations

  1. McMaster University, Hamilton, ON, Canada

    William M. Farmer & Qian Hu

Authors
  1. William M. Farmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Qian Hu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to William M. Farmer .

Editor information

Editors and Affiliations

  1. SPAWAR Systems Center Pacific, San Diego, California, USA

    Stuart H. Rubin

  2. Laboratoire de Communication dans les Systèmes Informatiques, Ecole nationale Supérieure d’Informatique, Algiers, Algeria

    Thouraya Bouabana-Tebibel

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

Farmer, W.M., Hu, Q. (2018). FCL: A Formal Language for Writing Contracts. In: Rubin, S., Bouabana-Tebibel, T. (eds) Quality Software Through Reuse and Integration. FMI IRI 2016 2016 2016. Advances in Intelligent Systems and Computing, vol 561. Springer, Cham. https://doi.org/10.1007/978-3-319-56157-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-56157-8_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-56156-1

  • Online ISBN: 978-3-319-56157-8

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation