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 104 articles , 1 standard article )

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

1 2 3 4 5 6 next

  1. Haveraaen, Magne; Järvi, Jaakko: Semantics of multiway dataflow constraint systems (2021)
  2. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
  3. Riesco, Adrián; Ogata, Kazuhiro: A formal proof generator from semi-formal proof documents (2017)
  4. Futatsugi, Kokichi: Generic proof scores for generate & check method in CafeOBJ (2015)
  5. Futatsugi, Kokichi: Generate & check method for verifying transition systems in CafeOBJ (2015)
  6. Eden, A. H.; Gasparis, E.; Nicholson, J.; Kazman, R.: Modeling and visualizing object-oriented programs with Codecharts (2013)
  7. Jones, Cliff B.; Freitas, Leo; Velykis, Andrius: Ours \textitisto reason why (2013)
  8. Hatcliff, John; Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  9. Khan, Muhammad Taimoor; Schreiner, Wolfgang: Towards the formal specification and verification of Maple programs (2012)
  10. Sannella, Donald; Tarlecki, Andrzej: Foundations of algebraic specification and formal software development. (2012)
  11. Logozzo, Francesco: Class invariants as abstract interpretation of trace semantics (2009)
  12. Schröder, Lutz; Mossakowski, Till: HasCasl: integrated higher-order specification and program development (2009)
  13. Bidoit, Michel; Sannella, Donald; Tarlecki, Andrzej: Observational interpretation CASL specifications (2008)
  14. Ferrari, Mauro; Fiorentini, Camillo; Momigliano, Alberto; Ornaghi, Mario: Snapshot generation in a constructive object-oriented modeling language (2008)
  15. Middelkoop, Ronald; Huizing, Cornelis; Kuiper, Ruurd; Luit, Erik J.: Specification and verification of invariants by exploiting layers in OO designs (2008)
  16. Berger, Martin; Honda, Kohei; Yoshida, Nobuko: A logical analysis of aliasing in imperative higher-order functions (2007)
  17. Chalin, Patrice: Are the logical foundations of verifying compiler prototypes matching user expectations? (2007)
  18. Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
  19. Leino, K. Rustan M.; Schulte, Wolfram: A verifying compiler for a multi-threaded object-oriented language (2007)
  20. Lim, Hongping; Archer, Myla: Translation templates to support strategy development in PVS (2007)

1 2 3 4 5 6 next