PlusCal

from Wikipedia, the free encyclopedia

PlusCal is a formal language developed by Leslie Lamport for specifying concurrent algorithms and systems. It is a declarative language, where language constructs are designed in such a way that they are very similar to an imperative language. The syntax, which is more reminiscent of an imperative programming language, is intended to make it easier for programmers to use a formal language for specification. The aim here is to replace pseudocode that is not uniformly specified and therefore ambiguous .

There are two different syntax versions of PlusCal. The C syntax, where c stands for compact , is a compact variant that uses brackets in many places to mark the beginning and the end of blocks. It is intended for programmers who use the programming languages C , C ++ , C # or Java . The P syntax, where p stands for prolix , uses terms like begin and end instead of brackets .

PlusCal is based on TLA + , which means that TLA + expressions can be used in PlusCal. In addition, PlusCal specifications can be translated into TLA + for subsequent review with TLC . A corresponding translation program is part of the TLA + Toolbox . In addition to a translation program, the TLA + Toolbox also contains a program for setting PlusCal specifications in LaTeX .

PlusCal is used, among other things, in the development of Amazon Web Services .

literature

  • Leslie Lamport: The PlusCal Algorithm Language . In: Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (=  ICTAC '09 ). Springer-Verlag, Berlin, Heidelberg 2009, ISBN 978-3-642-03465-7 , pp. 36–60 , doi : 10.1007 / 978-3-642-03466-4_2 ( research.microsoft.com [PDF; accessed October 31, 2015]).
  • Leslie Lamport: Checking a Multithreaded Algorithm with + CAL . In: Proceedings of the 20th International Conference on Distributed Computing (=  DISC'06 ). Springer-Verlag, Berlin, Heidelberg 2006, ISBN 3-540-44624-9 , pp. 151–163 , doi : 10.1007 / 11864219_11 ( research.microsoft.com [PDF; accessed October 31, 2015]).
  • Leslie Lamport: A PlusCal User's Manual . C syntax ∗ Version 1.8. Microsoft Research, October 21, 2015 ( research.microsoft.com [PDF; accessed October 31, 2015]).
  • Leslie Lamport: A PlusCal User's Manual . P-syntax ∗ Version 1.8. Microsoft Research, October 21, 2015 ( research.microsoft.com [PDF; accessed October 31, 2015]).

Web links

Individual evidence

  1. ↑ Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff: How Amazon Web Services Uses Formal Methods . In: Commun. ACM . tape 58 , no. 4 , March 2015, ISSN  0001-0782 , p. 66-73 , doi : 10.1145 / 2699417 .