Abstract
This paper introduces a specification construct that is fitting when combining verified code with unverified code. The specification is a form of precondition that imposes proof obligations for both callers and callees. This precondition,
, blends in well with the parameter-validation conventions in Java and with the syntax and semantics of specification languages such as JML, ACSL, and Dafny.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This coincides with the interpretation of
clauses in Dafny. In JML, frames are defined using
clauses, and an absent
clause means
. For our discussion here,
is more convenient as a default. .
- 2.
JML uses an operator called
to combine specifications. It gives a nice way to express what we write with
in this paper. Nevertheless, we chose not to use the
operator in this paper, because
in essence uses
clauses for the guards. By using the
notation in this paper, we avoid any confusion regarding
and
in this context.
- 3.
Some methods in Java 11, like java.lang.System.arraycopy (https://docs.oracle.com/javase/7/docs/api/java/lang/System.html), spell out the order, whereas many others, like javax.crypto.Cipher.getInstance (https://docs.oracle.com/javase/7/docs/api/javax/crypto/Cipher.html), do not.
- 4.
Since the second
group has an empty
clause,
is the same as A. Nevertheless, we will continue to write
to emphasize that we’re referring to the value of A on entry to the method.
- 5.
The
keyword avoids the default situation in JML in which Value is implicitly a non-null type. We use it in this section, since the focus of our discussion is on using specifications for parameter validation.
- 6.
In other words, the
statement trades a verification assumption for a run-time check. The run-time behavior of an
statement is similar to an always-enabled
statement in Java, but from the verification perspective, the
condition is checked by the verifier whereas the
condition is assumed by the verifier.
References
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification—The KeY Book—From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6
Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Comm. ACM 54(6), 81–91 (2011). https://doi.org/10.1145/1953122.1953145
Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Comm. ACM 64(8), 56–68 (2021). https://doi.org/10.1145/3470569
Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35
Cok, D.R.: JML and OpenJML for Java 16. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, pp. 65–67. ACM (2021). https://doi.org/10.1145/3464971.3468417
Cok, D.R., Leavens, G.T., Ulbrich, M.: JML Reference Manual, 2nd edn. (2021). https://www.openjml.org/documentation/JML_Reference_Manual.pdf
ECMA International: Eiffel: Analysis, Design and Programming Language, 2nd edn., June 2006. Standard ECMA-367
Goodenough, J.B.: Structured exception handling. In: Graham, R.M., Harrison, M.A., Reynolds, J.C. (eds.) Conference Record of the Second ACM Symposium on Principles of Programming Languages, pp. 204–224. ACM, January 1975. https://doi.org/10.1145/512976.512997
Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Boston (1996)
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012). https://doi.org/10.1145/2187671.2187678. Article 16
Klabnik, S., Nichols, C.: The Rust Programming Language (2018). https://doc.rust-lang.org/book/
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94–97 (2017). https://doi.org/10.1109/MS.2017.4121212
Leino, K.R.M., Ford, R.L., Cok, D.R.: Dafny reference manual (2021). https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef
Leino, K.R.M., Schulte, W.: Exception safety for C#. In: Cuellar, J.R., Liu, Z. (eds.) SEFM 2004–Second International Conference on Software Engineering and Formal Methods, pp. 218–227. IEEE, September 2004. https://doi.org/10.1109/SEFM.2004.14
Meyer, B.: Object-oriented Software Construction. Series in Computer Science, Prentice-Hall International, Hoboken (1988)
Acknowledgments
We thank Serdar Tasiran for suggesting the keyword
as a good description of the alternative precondition. We are grateful to the reviewers and Mattias Ulbrich for useful comments on a draft of this paper. Happy birthday, Reiner Hähnle, and thank you for your groundbreaking contributions to verifying software and the tooling that is taking us there.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Cok, D.R., Leino, K.R.M. (2022). Specifying the Boundary Between Unverified and Verified Code. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds) The Logic of Software. A Tasting Menu of Formal Methods. Lecture Notes in Computer Science, vol 13360. Springer, Cham. https://doi.org/10.1007/978-3-031-08166-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-031-08166-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-08165-1
Online ISBN: 978-3-031-08166-8
eBook Packages: Computer ScienceComputer Science (R0)