LARCH

The Larch family of languages supports a two-tiered, definitional style of specification. Each specification has components written in two languages: one language that is designed for a specific programming language and another language that is independent of any programming language. The former kind are Larch interface languages, and the latter is the Larch Shared Language (LSL). Interface languages are used to specify the interfaces between program components. Each specification provides the information needed to use an interface. A critical part of each interface is how components communicate across the interface. Communication mechanisms differ from programming language to programming language. For example, some languages have mechanisms for signalling exceptional conditions, other do not. More subtle differences arise from the various parameter passing and storage allocation mechanisms used by different languages. It is easier to be precise about communication when the interface specification language reflects the programming language. Each interface language deals with what can be observed by client programs written in a particular programming language. Larch interface languages have been designed for a variety of programming languages, including Ada, C, C++, CLU, CORBA, ML, Modula-3, and Smalltalk. There are also ”generic” Larch interface languages that can be specialized for particular programming languages or used to specify interfaces between programs in different languages. Interface specifications rely on definitions from auxiliary specifications, written in LSL, to provide semantics for the primitive terms they use. Specifiers are not limited to a fixed set of notations, but can use LSL to define specialized vocabularies suitable for particular interface specifications or classes of specifications.


References in zbMATH (referenced in 78 articles , 1 standard article )

Showing results 1 to 20 of 78.
Sorted by year (citations)

1 2 3 4 next

  1. Eden, A.H.; Gasparis, E.; Nicholson, J.; Kazman, R.: Modeling and visualizing object-oriented programs with Codecharts (2013)
  2. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  3. Khan, Muhammad Taimoor; Schreiner, Wolfgang: Towards the formal specification and verification of Maple programs (2012)
  4. Sannella, Donald; Tarlecki, Andrzej: Foundations of algebraic specification and formal software development. (2012)
  5. Schröder, Lutz; Mossakowski, Till: HasCasl: integrated higher-order specification and program development (2009)
  6. Ferrari, Mauro; Fiorentini, Camillo; Momigliano, Alberto; Ornaghi, Mario: Snapshot generation in a constructive object-oriented modeling language (2008)
  7. Middelkoop, Ronald; Huizing, Cornelis; Kuiper, Ruurd; Luit, Erik J.: Specification and verification of invariants by exploiting layers in OO designs (2008)
  8. Berger, Martin; Honda, Kohei; Yoshida, Nobuko: A logical analysis of aliasing in imperative higher-order functions (2007)
  9. Chalin, Patrice: Are the logical foundations of verifying compiler prototypes matching user expectations? (2007)
  10. Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
  11. Leino, K.Rustan M.; Schulte, Wolfram: A verifying compiler for a multi-threaded object-oriented language (2007)
  12. Lim, Hongping; Archer, Myla: Translation templates to support strategy development in PVS. (2007)
  13. Mousavi, Mohammadreza; Reniers, Michel A.; Groote, Jan Friso: SOS formats and meta-theory: 20 years after (2007)
  14. Ogata, Kazuhiro; Futatsugi, Kokichi: Modeling and verification of real-time systems based on equations (2007)
  15. Müller, Peter; Poetzsch-Heffter, Arnd; Leavens, Gary T.: Modular invariants for layered object structures (2006)
  16. Ogata, Kazuhiro; Futatsugi, Kokichi: Some tips on writing proof scores in the OTS/CafeOBJ method (2006)
  17. Poetzsch-Heffter, Arnd; Schäfer, Jan: Modular specification of encapsulated object-oriented components (2006)
  18. Seino, Takahiro; Ogata, Kazuhiro; Futatsugi, Kokichi: A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method. (2006)
  19. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K.Rustan M.; Poll, Erik: An overview of JML tools and applications (2005)
  20. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K.Rustan M.; Poll, Erik: An overview of JML tools and applications (2005)

1 2 3 4 next