First International Workshop on Larch: Proceedings of the First International Workshop on Larch, Dedham, Massachusetts, USA, 13–15 July 1992

مقالات این جلد در اولین کارگاه بین‌المللی در مورد کاج اروپایی، که در MIT Endicott House در نزدیکی بوستون در 13 تا 15 ژوئیه 1992 برگزار شد، ارائه شد. Larch یک خانواده از زبان‌ها و ابزارهای مشخصات رسمی است و این کارگاه انجمنی برای کسانی که زبان های Larch را طراحی کرده اند، پشتیبانی ابزاری برای آنها ساخته اند، به ویژه Larch Prover، و از آنها برای مشخص کردن و استدلال در مورد سیستم های نرم افزاری و سخت افزاری استفاده می کنند. پروژه Larch در سال 1980 به رهبری جان گوتاگ در MIT و جیمز هورنینگ، سپس در مرکز تحقیقات زیراکس/پالو آلتو و اکنون در شرکت تجهیزات دیجیتال/مرکز تحقیقات سیستم‌ها (DEC/SRC) آغاز شد. کاربردهای اصلی شامل سنتز مدار VLSI، ارتباطات دستگاه پزشکی، توسعه کامپایلر و سیستم‌های همزمان مبتنی بر TLA Lamport و همچنین چندین کاربرد برای اثبات قضیه کلاسیک و مشخصات جبری است. Larch از یک رویکرد دو لایه برای تعیین ماژول های نرم افزاری و سخت افزاری پشتیبانی می کند. یک ردیف از مشخصات در زبان مشترک لچ (LSL) نوشته شده است. مشخصات LSL انتزاعات ریاضی مانند مجموعه ها، روابط و جبرها را توصیف می کند. معناشناسی آن بر اساس نظریه های مرتبه اول تعریف می شود. لایه دوم به زبان رابط Larch نوشته شده است، یکی برای یک زبان برنامه نویسی خاص طراحی شده است. یک مشخصات رابط، اثرات تک تک ماژول ها را توصیف می کند، به عنوان مثال. تغییرات حالت، تخصیص منابع و استثنائات. معناشناسی آن بر حسب محمولات مرتبه اول بر دو حالت تعریف می شود، که در آن حالت بر حسب مفهوم حالت زبان برنامه نویسی تعریف می شود. بنابراین، LSL مستقل از زبان برنامه نویسی است. یک زبان رابط Larch وابسته به زبان برنامه نویسی است.

The papers in this volume were presented at the First International Workshop on Larch, held at MIT Endicott House near Boston on 13-15 July 1992. Larch is a family of formal specification languages and tools, and this workshop was a forum for those who have designed the Larch languages, built tool support for them, particularly the Larch Prover, and used them to specify and reason about software and hardware systems. The Larch Project started in 1980, led by John Guttag at MIT and James Horning, then at Xerox/Palo Alto Research Center and now at Digital Equipment Corporation/Systems Research Center (DEC/SRC). Major applications have included VLSI circuit synthesis, medical device communications, compiler development and concurrent systems based on Lamport's TLA, as well as several applications to classical theorem proving and algebraic specification. Larch supports a two-tiered approach to specifying software and hardware modules. One tier of a specification is wrillen in the Larch Shared Language (LSL). An LSL specification describes mathematical abstractions such as sets, relations, and algebras; its semantics is defined in terms of first-order theories. The second tier is written in a Larch interface language, one designed for a specific programming language. An interface specification describes the effects of individual modules, e.g. state changes, resource allocation, and exceptions; its semantics is defined in terms of first-order predicates over two states, where state is defined in terms of the programming language's notion of state. Thus, LSL is programming language independent; a Larch interface language is programming language dependent.