Abstract
The KeY system accepts different kinds of inputs related to Java Card DL. From the user point of view these inputs can be divided into the following categories:
-
system rule files,
-
user defined rule files,
-
user problem files/proofs with optional user defined rules,
-
Java Card DL terms and formulae required by the interaction component of the KeY system.
From the system’s perspective the division is similar, but on top of this, the distinction between schematic mode and term (normal) mode is very important:
-
in schematic mode schema variables can be defined and used (usually in definition of rules/taclets) and concrete terms or formulae are forbidden,
-
in normal mode schema variables and all other schematic constructs are forbidden, while concrete terms and formulae are allowed.
Additionally, most of terms and formulae constructs can appear in both schematic and normal mode, but take slightly different form depending on the mode.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this chapter
Cite this chapter
Mostowski, W. (2007). The KeY Syntax. In: Beckert, B., Hähnle, R., Schmitt, P.H. (eds) Verification of Object-Oriented Software. The KeY Approach. Lecture Notes in Computer Science(), vol 4334. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69061-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-69061-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68977-5
Online ISBN: 978-3-540-69061-0
eBook Packages: Computer ScienceComputer Science (R0)