[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Constructing the Views Framework

  • Conference paper
  • First Online:
Unifying Theories of Programming (UTP 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8963))

Included in the following conference series:

Abstract

The views framework of Dinsdale-Young and others unifies several compositional techniques for reasoning about concurrent programs. This paper uses simple mathematics to construct the views framework incrementally from first principles. The result is a model for the views framework, which can also be understood as an independent theory of concurrent programs. Along the lines of “sequential programs are binary relations”, the theory adopts the maxim “concurrent programs are formal languages”. Consequently, programs obey familiar algebraic laws that can simplify reasoning; there is no need to postulate operational rules; the views program logic can be constructed in a stepwise fashion from more basic logics; program logic and operational thinking become largely decoupled; proving partial correctness becomes straightforward and it holds irrespectively of the specific choice of programming language constructs, operational rules, and the atomic actions that are implemented in a computer. All theorems have been formally checked with Isabelle/HOL. A proof script is available online.

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

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 27.99
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 34.99
Price includes VAT (United Kingdom)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013. ACM, New York, pp. 287–300 (2013)

    Google Scholar 

  2. Isabelle/HOL proofs (2014). http://www0.cs.ucl.ac.uk/staff/s.vanstaden/proofs/Views.tgz

  3. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  4. Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bloom, S.L., Ésik, Z.: Free shuffle algebras in language varieties. Theoretical Computer Science 163(1–2), 55–98 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  6. Hoare, T., van Staden, S.: The laws of programming unify process calculi. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 7–22. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Hoare, T., van Staden, S.: In praise of algebra. Formal Aspects of Computing 24, 423–431 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  8. van Staden, S., Hoare, T.: Algebra unifies operational calculi. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 88–104. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Park, D.: On the semantics of fair parallelism. In: Bjørner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  10. Brookes, S.: Full abstraction for a shared-variable parallel language. Information and Computation 127(2), 145–163 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  11. Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (September 1981)

    Google Scholar 

  12. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer (1980)

    Google Scholar 

  13. Kahn, G.: Natural semantics. In: Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS 1987. Springer, London, pp. 22–39 (1987)

    Google Scholar 

  14. Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction (July 1999). http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html (Original edition published 1992 by John Wiley & Sons) (revised edition)

  15. Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On locality and the exchange law for concurrent processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Stephan van Staden .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

van Staden, S. (2015). Constructing the Views Framework. In: Naumann, D. (eds) Unifying Theories of Programming. UTP 2014. Lecture Notes in Computer Science(), vol 8963. Springer, Cham. https://doi.org/10.1007/978-3-319-14806-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-14806-9_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-14805-2

  • Online ISBN: 978-3-319-14806-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics