US 11,921,616 B1
Retaining Dafny specifications
Tongtong Xiang, Seattle, WA (US); Sean Mclaughlin, Seattle, WA (US); Marianna Rapoport, Toronto (CA); Neha Rungta, San Jose, CA (US); Matthias Schlaipfer, Berlin (DE); and Florian Rabe, Erlangen (DE)
Assigned to Amazon Technologies, Inc., Seattle, WA (US)
Filed by Amazon Technologies, Inc., Seattle, WA (US)
Filed on Mar. 29, 2022, as Appl. No. 17/707,861.
Int. Cl. G06F 11/36 (2006.01); G06F 8/35 (2018.01); G06F 8/41 (2018.01); G06F 9/445 (2018.01)
CPC G06F 11/3628 (2013.01) [G06F 8/35 (2013.01); G06F 8/447 (2013.01); G06F 9/44589 (2013.01)] 23 Claims
OG exemplary drawing
 
1. A method, comprising:
initiating, with a compiler, a compiling of a first code written in a Dafny programming language to a second code written in a Java programming language;
detecting, as part of the compiling, a specification included in the first code;
compiling the specification into at least one of an annotation that is understandable to a verification component, an expression that is understandable to the verification component, a comment that is understandable to the verification component, or an assertion that is understandable to the verification component;
including the at least one of the annotation, the expression, the comment, or the assertion in the second code; and
verifying, with the verification component, the second code, wherein the verification component utilizes the at least one of the annotation, the expression, the comment, or the assertion to verify at least a portion of the second code.