More Web Proxy on the site http://driver.im/

article

Semantic essence of AsmL

Authors:

Benjamin Rossman,

Wolfram SchulteAuthors Info & Claims

Theoretical Computer Science, Volume 343, Issue 3

Pages 370 - 412

https://doi.org/10.1016/j.tcs.2005.06.017

Published: 17 October 2005 Publication History

Abstract

The Abstract State Machine Language, AsmL, is a novel executable specification language based on the theory of Abstract State Machines. AsmL is object-oriented, provides high-level mathematical data-structures, and is built around the notion of synchronous updates and finite choice. AsmL is fully integrated into the .NET framework and Microsoft development tools. In this paper, we explain the design rationale of AsmL and provide static and dynamic semantics for a kernel of the language.

References

[1]

{1} The AsmL webpage, http://research.microsoft.com/foundations/AsmL/.]]

[2]

{2} D. Bjoerner, C.B. Jones (Eds.), Formal Specification and Software Development, Prentice-Hall International, Englewood Cliff, NJ, 1982.]]

[3]

{3} A. Blass, Y. Gurevich, Ordinary interactive small-step algorithms, I, ACM Trans. Comput. Logic, to appear. See Microsoft Research Tech. Report MSR-TR-2004-16.]]

Digital Library

[4]

{4} A. Blass, Y. Gurevich, Ordinary Interactive Small-Step Algorithms, II, Microsoft Research, Tech. Report MSR-TR-2004-88.]]

[5]

{5} A. Blass, Y. Gurevich, S. Shelah, Choiceless polynomial time, Ann. Pure Appl. Logic 100 (1999) 141-187.]]

[6]

{6} E. Boerger, J. Schmid, Composition and submachine concepts for sequential ASMs, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic (Proc. CSL 2000), Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 41-60.]]

Digital Library

[7]

{8} M.J.C. Gordon, T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, Cambridge, 1993.]]

Digital Library

[8]

{9} Y. Gurevich, Evolving algebra 1993: Lipari guide, in: E. Boerger (Ed.), Specification and Validation Methods, Oxford University Press, Oxford, 1995, pp. 9-36.]]

Digital Library

[9]

{10} Y. Gurevich, May 1997 draft of the ASM guide, Tech. Report CSE-TR-336-97, EECS Department, University of Michigan, 1997 (available at the author's website).]]

[10]

{11} Y. Gurevich, For every sequential algorithm there is an equivalent sequential abstract state machine, ACM Trans. Comput. Logic 1 (1) (2000) 77-111.]]

Digital Library

[11]

{12} Y. Gurevich, W. Schulte, M. Veanes, Toward Industrial Strength Abstract State Machines, Tech. Report MSR-TR-2001-98, Microsoft Research, October 2001.]]

[12]

{13} Y. Gurevich, N. Tillmann, Partial updates: exploration, Springer J. Universal Comput. Sci. 7 (11) (2001) 918-952.]]

[13]

{14} A. Hejlsberg, S. Wiltamutch, P. Golde, The C# Programming Language, Addison-Wesley, Reading, MA, 2003.]]

[14]

{15} P. Hudak, S.P. Jones, P. Wadler, B. Boutel, J., Fairbairn, J. Fasel, M.M. Guzman, K. Hammond, J. Hughes, T. Johnsson, D. Kieburtz, R. Nikhil, W. Partain, J. Peterson, Report on the Programming Language Haskell, Version 1.2, SIGPLAN Notices 27 (5) May 1992.]]

Digital Library

[15]

{16} J.K. Huggins, ASM Michigan web page, http://www.eecs.umich.edu/gasm.]]

[16]

{17} A. Igarashi, B.C. Pierce, P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Trans. Program. Languages Systems (TOPLAS) 23 (3) (2001) 396-450.]]

Digital Library

[17]

{18} B. Joy, G. Steele, J. Gosling, G. Bracha, Java (TM) Language Specification, 2nd ed., Addison-Wesley, Reading, MA, 2000.]]

[18]

{19} G. Kahn, Natural semantics, in: Proc. Symp. on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Vol. 247, 1987, pp. 22-39.]]

Digital Library

[19]

{20} R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), MIT Press, Cambridge, MA, 1997.]]

Digital Library

[20]

{21} Objective Caml Website http://www.ocaml.org/.]]

[21]

{22} M. Odersky, P. Wadler, Pizza into Java: translating theory into practice, Proc. 24th ACM Symp. on Principles of Programming Languages, Paris, France, January 1997.]]

Digital Library

[22]

{23} B.C. Pierce, Types and Programming Languages, MIT Press, Cambridge, MA, 2002.]]

Digital Library

[23]

{24} G.D. Plotkin, Structural approach to operational semantics, Tech. Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark, September 1981.]]

[24]

{25} PVS Website http://pvs.csl.sri.com/.]]

[25]

{26} J.M. Spivey, The Z Notation: A Reference Manual, 2nd ed., Prentice-Hall, New York, 1992.]]

Digital Library

Cited By

Couderc NReichenbach CSöderberg E(2023)Classification-based Static Collection Selection for Java: Effectiveness and AdaptabilityProceedings of the 27th International Conference on Evaluation and Assessment in Software Engineering10.1145/3593434.3593469(111-120)Online publication date: 14-Jun-2023
https://dl.acm.org/doi/10.1145/3593434.3593469
Bevilacqua GBianchi APérez JMirandola RChen H(2018)MOTIONProceedings of the 12th European Conference on Software Architecture: Companion Proceedings10.1145/3241403.3241444(1-4)Online publication date: 24-Sep-2018
https://dl.acm.org/doi/10.1145/3241403.3241444
Broy MHavelund KKumar RSteffen B(2018)Towards a Unified View of Modeling and Programming (ISoLA 2018 Track Introduction)Leveraging Applications of Formal Methods, Verification and Validation. Modeling10.1007/978-3-030-03418-4_1(3-21)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1007/978-3-030-03418-4_1
Show More Cited By

Index Terms

Semantic essence of AsmL
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Constructive semantics
A semantic and methodological essence of message sequence charts

Message sequence charts (MSCs) are a technique to describe patterns of interaction between the components of interactive distributed systems by specific interaction diagrams. MSCs have evolved in telecommunication applications, defined as a standard, ...
Generating formal specifications for security-critical applications - A model-driven approach
IWSESS '09: Proceedings of the 2009 ICSE Workshop on Software Engineering for Secure Systems

The SecureMDD approach aims to generate both, a formal specification for verification and executable code, from UML diagrams. The UML models define the static as well as dynamic components of the system under development. This model-driven approach is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 343, Issue 3

Formal methods for components and objects

17 October 2005

246 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 17 October 2005

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Couderc NReichenbach CSöderberg E(2023)Classification-based Static Collection Selection for Java: Effectiveness and AdaptabilityProceedings of the 27th International Conference on Evaluation and Assessment in Software Engineering10.1145/3593434.3593469(111-120)Online publication date: 14-Jun-2023
https://dl.acm.org/doi/10.1145/3593434.3593469
Bevilacqua GBianchi APérez JMirandola RChen H(2018)MOTIONProceedings of the 12th European Conference on Software Architecture: Companion Proceedings10.1145/3241403.3241444(1-4)Online publication date: 24-Sep-2018
https://dl.acm.org/doi/10.1145/3241403.3241444
Broy MHavelund KKumar RSteffen B(2018)Towards a Unified View of Modeling and Programming (ISoLA 2018 Track Introduction)Leveraging Applications of Formal Methods, Verification and Validation. Modeling10.1007/978-3-030-03418-4_1(3-21)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1007/978-3-030-03418-4_1
Beierle C(2016)Systems and Implementations for Solving Reasoning Problems in Conditional LogicsProceedings of the 9th International Symposium on Foundations of Information and Knowledge Systems - Volume 961610.1007/978-3-319-30024-5_5(83-94)Online publication date: 7-Mar-2016
https://dl.acm.org/doi/10.1007/978-3-319-30024-5_5
Lezuo RPaulweber PKrall A(2014)CASMACM SIGPLAN Notices10.1145/2666357.259781349:5(13-22)Online publication date: 12-Jun-2014
https://dl.acm.org/doi/10.1145/2666357.2597813
Lezuo RPaulweber PKrall AZhang YKulkarni P(2014)CASMProceedings of the 2014 SIGPLAN/SIGBED conference on Languages, compilers and tools for embedded systems10.1145/2597809.2597813(13-22)Online publication date: 12-Jun-2014
https://dl.acm.org/doi/10.1145/2597809.2597813
Zenzaro SGervasi VSoldani J(2014)WebASMProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_19(216-221)Online publication date: 2-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-662-43652-3_19
Jeannin Jde Caso GChen JGurevich YNaldurg PSwamy N(2013)DKAL*Proceedings of the 5th international conference on Engineering Secure Software and Systems10.1007/978-3-642-36563-8_10(139-154)Online publication date: 27-Feb-2013
https://dl.acm.org/doi/10.1007/978-3-642-36563-8_10
Veanes MBjØrner N(2012)Alternating simulation and IOCOInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3115963.311608414:4(387-405)Online publication date: 1-Aug-2012
https://dl.acm.org/doi/10.5555/3115963.3116084
Badreddin OLethbridge TBegel ASadowski C(2012)Combining experiments and grounded theory to evaluate a research prototypeProceedings of the First International Workshop on User Evaluation for Software Engineering Researchers10.5555/2667089.2667090(1-4)Online publication date: 5-Jun-2012
https://dl.acm.org/doi/10.5555/2667089.2667090
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents