verifast-docs

Java Translation Units

VeriFast supports most of Java 1.0. More specifically, VeriFast accepts .java files that match the CompilationUnit production of the grammar below. (Based on Chapter 19 of JLS21.)

Literal:
  IntegerLiteral
  FloatingPointLiteral
  BooleanLiteral
  CharacterLiteral
  StringLiteral
  TextBlock
  NullLiteral

Type:
  PrimitiveType
  ReferenceType
  Identifier [TypeArguments]
  real
  fixpoint ( TypeArgumentList )
  predicate PredicateParameters
  any

PrimitiveType:
  NumericType
  boolean

NumericType:
  IntegralType
  FloatingPointType

IntegralType:
  (one of)
  byte short int long char

FloatingPointType:
  (one of)
  float double

ReferenceType:
  ClassOrInterfaceType
  TypeVariable
  ArrayType

ClassOrInterfaceType:
  ClassType
  InterfaceType

ClassType:
  TypeIdentifier [TypeArguments]
  PackageName . TypeIdentifier [TypeArguments]

InterfaceType:
  ClassType

TypeVariable:
  TypeIdentifier

ArrayType:
  PrimitiveType Dims
  ClassOrInterfaceType Dims
  TypeVariable Dims

Dims:
  [ ] {[ ]}

TypeParameter:
  TypeIdentifier [TypeBound]

TypeArguments:
  < TypeArgumentList >

TypeArgumentList:
  TypeArgument {, TypeArgument}

TypeArgument:
  ReferenceType
  Wildcard

PackageName:
  Identifier
  PackageName . Identifier

TypeName:
  TypeIdentifier
  PackageOrTypeName . TypeIdentifier

ExpressionName:
  Identifier
  AmbiguousName . Identifier

MethodName:
  UnqualifiedMethodIdentifier

PackageOrTypeName:
  Identifier
  PackageOrTypeName . Identifier

AmbiguousName:
  Identifier
  AmbiguousName . Identifier

CompilationUnit:
  OrdinaryCompilationUnit
  ModularCompilationUnit

OrdinaryCompilationUnit:
  [PackageDeclaration] {ImportDeclaration} {TopLevelDeclaration}

PackageDeclaration:
  package Identifier {. Identifier} ;

ImportDeclaration:
  SingleTypeImportDeclaration
  TypeImportOnDemandDeclaration
  SingleStaticImportDeclaration
  StaticImportOnDemandDeclaration

SingleTypeImportDeclaration:
  import TypeName ;

TypeImportOnDemandDeclaration:
  import PackageOrTypeName . * ;

TopLevelDeclaration:
  TopLevelClassOrInterfaceDeclaration
  GhostDeclarationBlock

TopLevelClassOrInterfaceDeclaration:
  ClassDeclaration
  InterfaceDeclaration
  ;

ClassDeclaration:
  NormalClassDeclaration
  EnumDeclaration
  RecordDeclaration

NormalClassDeclaration:
  {ClassModifier} class TypeIdentifier [TypeParameters[ [ClassExtends] [ClassImplements] [ClassPermits] ClassBody

ClassModifier:
  (one of)
  Annotation public protected private
  abstract static final sealed non-sealed strictfp

TypeParameters:
  < TypeParameterList >

TypeParameterList:
  TypeParameter {, TypeParameter}

ClassExtends:
  extends ClassType

ClassImplements:
  implements InterfaceTypeList

InterfaceTypeList:
  InterfaceType {, InterfaceType}

ClassBody:
  { {ClassBodyDeclaration} }

ClassBodyDeclaration:
  ClassMemberDeclaration
  InstanceInitializer
  StaticInitializer
  ConstructorDeclaration

ClassMemberDeclaration:
  FieldDeclaration
  MethodDeclaration
  ClassDeclaration
  InterfaceDeclaration
  ;

FieldDeclaration:
  {FieldModifier} Type VariableDeclaratorList ;

FieldModifier:
  (one of)
  Annotation public protected private
  static final transient volatile

VariableDeclaratorList:
  VariableDeclarator {, VariableDeclarator}

VariableDeclarator:
  VariableDeclaratorId [= VariableInitializer]

VariableDeclaratorId:
  Identifier [Dims]

VariableInitializer:
  Expression
  ArrayInitializer

MethodDeclaration:
  {MethodModifier} MethodHeader MethodBody

MethodModifier:
  (one of)
  Annotation public protected private
  abstract static final synchronized native strictfp

MethodHeader:
  Result MethodDeclarator [Throws] {SpecificationClause}
  TypeParameters {Annotation} Result MethodDeclarator [Throws]

Result:
  Type
  void

MethodDeclarator:
  Identifier ( [FormalParameterList] ) [Dims]

FormalParameterList:
  FormalParameter {, FormalParameter}

FormalParameter:
  {VariableModifier} Type VariableDeclaratorId
  VariableArityParameter

Throws:
  throws ExceptionTypeList

ExceptionTypeList:
  ExceptionType {, ExceptionType}

ExceptionType:
  ClassType
  TypeVariable

SpecificationClause:
  /*@ SpecificationGhostClause @*/
  SpecificationGhostClause

SpecificationGhostClause:
  nonghost_callers_only
  : Identifier [( ArgumentList )]
  requires Assertion ;
  ensures Assertion ;
  terminates ;

MethodBody:
  Block
  ;

ConstructorDeclaration:
  {ConstructorModifier} ConstructorDeclarator [Throws] ConstructorBody

ConstructorModifier:
  (one of)
  Annotation public protected private

ConstructorDeclarator:
  [TypeParameters] SimpleTypeName ( [FormalParameterList] )

SimpleTypeName:
  TypeIdentifier

ConstructorBody:
  { [ExplicitConstructorInvocation] [BlockStatements] }

ExplicitConstructorInvocation:
  [TypeArguments] this ( [ArgumentList] ) ;
  [TypeArguments] super ( [ArgumentList] ) ;
  ExpressionName . [TypeArguments] super ( [ArgumentList] ] ;
  Primary . [TypeArguments] super ( [ArgumentList] ) ;

InterfaceDeclaration:
  NormalInterfaceDeclaration
  AnnotationInterfaceDeclaration

NormalInterfaceDeclaration:
  {InterfaceModifier} interface TypeIdentifier [TypeParameters] [InterfaceExtends] [InterfacePermits] InterfaceBody

InterfaceModifier:
  (one of)
  Annotation public protected private
  abstract static sealed non-sealed strictfp

InterfaceExtends:
  extends InterfaceTypeList

InterfaceBody:
  { {InterfaceMemberDeclaration} }

InterfaceMemberDeclaration:
  ConstantDeclaration
  InterfaceMethodDeclaration
  ClassDeclaration
  InterfaceDeclaration
  ;

ConstantDeclaration:
  {ConstantModifier} Type VariableDeclaratorList ;

ConstantModifier:
  (one of)
  Annotation public private
  abstract default static strictfp

InterfaceMethodDeclaration:
  {InterfaceMethodModifier} MethodHeader MethodBody

InterfaceMethodModifier:
  (one of)
  Annotation public private
  abstract default static strictfp

ArrayInitializer:
  { [VariableInitializerList] [,] }

VariableInitializerList:
  VariableInitializer {, VariableInitializer}

GhostDeclarationBlock:
  /*@ {GhostDeclaration} @*/

GhostDeclaration:
  InductiveDatatypeDeclaration
  FixpointFunctionDefinition
  PredicateDeclaration
  PredicateFamilyDeclaration
  FredicateFamilyInstanceDefinition
  PredicateConstructorDefinition
  LemmaFunctionDeclaration
  BoxClassDeclaration

InductiveDatatypeDeclaration:
  inductive Identifier [GenericParameters] = [|] InductiveDatatypeCase {| InductiveDatatypeCase} ;

GenericParameters:
  < Identifier {, Identifier} >

InductiveDatatypeCase:
  Identifier [ ( [FormalParameterList] ) ]

FixpointFunctionDefintion:
  fixpoint MethodDeclaration

PredicateDeclaration:
  predicate Identifier [GenericParameters] PredicateParameters ;
  PredicateKeyword Identifier [GenericParameters] PredicateParameters = Assertion ;

PredicateKeyword:
  predicate
  copredicate

PredicateParameters:
  ( [FormalParameterList] )
  ( [FormalParameterList] ; [FormalParameterList] )

PredicateFamilyDeclaration:
  predicate_family Identifier ( [FormalParameterList] ) PredicateParameters ;

PredicateFamilyInstanceDefinition:
  predicate_family_instance Identifier ( [ArgumentList] ) PredicateParameters = Assertion ;

PredicateConstructorDefinition:
  predicate_ctor Identifier ( FormalParameterList ) ( [FormalParameterList] ) = Assertion ;

LemmaFunctionDeclaration:
  LemmaKeyword MethodDeclaration

LemmaKeyword:
  lemma
  lemma_auto [( Expression )]

Block:
  { [BlockStatements] }

BlockStatements:
  BlockStatement {BlockStatement}

BlockStatement:
  LocalClassOrInterfaceDeclaration
  LocalVariableDeclarationStatement
  Statement

LocalVariableDeclarationStatement:
  LocalVariableDeclaration ;

LocalVariableDeclaration:
  {VariableModifier} LocalVariableType VariableDeclaratorList

LocalVariableType:
  Type
  var

Statement:
  StatementWithoutTrailingSubstatement
  LabeledStatement
  IfThenStatement
  IfThenElseStatement
  WhileStatement
  ForStatement

StatementNoShortIf:
  StatementWithoutTrailingSubstatement
  LabaledStatementNoShortIf
  IfThenElseStatementNoShortIf
  WhileStatementNoShortIf
  ForStatementNoShortIf

StatementWithoutTrailingSubstatement:
  Block
  EmptyStatement
  ExpressionStatement
  AssertStatement
  SwitchStatement
  DoStatement
  BreakStatement
  ContinueStatement
  ReturnStatement
  SynchronizedStatement
  ThrowStatement
  TryStatement
  YieldStatement
  GhostStatementBlock
  GhostStatement

EmptyStatement:
  ;

LabeledStatement:
  Identifier : Statement

LabeledStatementNoShortIf:
  Identifier : StatementNoShortIf

ExpressionStatement:
  StatementExpression ;

StatementExpression:
  Assignment
  PreIncrementExpression
  PreDecrementExpression
  PostIncrementExpression
  PostDecrementExpression
  MethodInvocation
  ClassInstanceCreationExpression

IfThenStatement:
  if ( Expression ) Statement

IfThenElseStatement:
  if ( Expression ) StatementNoShortIf else Statement

IfThenElseStatementNoShortIf:
  if ( Expression ) StatementNoShortIf else StatementNoShortIf

AssertStatement:
  assert Expression ;
  assert Expression : Expression ;

SwitchStatement:
  switch ( Expression ) SwitchBlock

SwitchBlock:
  { SwitchRule {SwitchRule} }
  { {SwitchBlockStatementGroup} {SwitchLabel :</i>}</i> }

SwitchBlockStatementGroup:
  SwitchLabel : {SwitchLabel :} BlockStatements

SwitchLabel:
  case CaseConstant {, CaseConstant}
  case null [, default]
  case CasePatterm [Guard]
  default
  case Identifier [( [Identifier {, Identifier}] )]

CaseConstant:
  ConditionalExpression

WhileStatement:
  while ( Expression ) {LoopAnnotation} Statement

WhileStatementNoShortIf:
  while ( Expression ) {LoopAnnotation} StatementNoShortIf

DoStatement:
  do {LoopAnnotation} Statement while ( Expression ) ;

ForStatement:
  BasicForStatement
  EnhancedForStatement

ForStatementNoShortIf:
  BasicForStatementNoShortIf
  EnhancedForStatementNoShortIf

BasicForStatement:
  for ( [ForInit] ; [Expression] ; [ForUpdate] ) {LoopAnnotation} Statement

BasicForStatementNoShortIf:
  for ( [ForInit] ; [Expression] ; [ForUpdate] ) {LoopAnnotation} StatementNoShortIf

ForInit:
  StatementExpressionList
  LocalVariableDeclaration

ForUpdate:
  StatementExpressionList

StatementExpressionList:
  StatementExpression {, StatementExpression}

LoopAnnotation:
  /*@ LoopGhostAnnotation @*/
  LoopGhostAnnotation

LoopGhostAnnotation:
  invariant Assertion ;
  requires Assertion ;
  ensures Assertion ;
  decreases Assertion ;

BreakStatement:
  break [Identifier] ;

ContinueStatement:
  continue [Identifier] ;

ReturnStatement:
  return [Expression] ;

ThrowStatement:
  throw Expression ;

TryStatement:
  try Block Catches
  try Block [Catches] Finally
  TryWithResourcesStatement

Catches:
  CatchClause {CatchClause}

CatchClause:
  catch ( CatchFormalParameter ) Block

CatchFormalParameter:
  {VariableModifier} CatchType VariableDeclaratorId

CatchType:
  ClassType {| ClassType}

Finally:
  finally Block

GhostStatementBlock:
  /*@ GhostStatement @*/

GhostStatement:
  open [Coefficient] PredicateAssertion ;
  close [Coefficient] PredicateAssertion ;
  leak Assertion ;
  invariant Assertion ;
  produce_lemma_function_pointer_chunk Identifier [TypeArguments] ( [ArgumentList] ) Identifiers Block Statement
  duplicate_lemma_function_pointer_chunk ( Expression ) ;
  produce_function_pointer_chunk Identifier [TypeArguments] ( Expression ) ( [ArgumentList] ) Identifiers Block
  merge_fractions Assertion ;
  SharedBoxesGhostStatement
  Statement

PrimaryAssertion:
  [Coefficient] PointsToAssertion
  [Coefficient] PredicateAssertion
  Expression
  switch ( Expression ) { {SwitchAssertionCase} }
  ( Assertion )
  forall_ ( Type Identifier ; Expression )
  emp

Coefficient:
  [ Pattern ]

PointsToAssertion:
  ConditionalExpression |-> Pattern

PredicateAssertion:
  Identifier [TypeArguments] [Patterns] Patterns

Patterns:
  ( [Pattern {, Pattern}] )

Pattern:
  _
  ? Identifier
  Identifier Patterns
  Expression
  ^ Expression

SwitchAssertionCase:
  case Identifier [Identifiers] : return Assertion ;

Assertion:
  PrimaryAssertion
  PrimaryAssertion &*& Assertion
  Expression ? Assertion : Assertion
  ensures Assertion

Primary:
  PrimaryNoNewArray
  ArrayCreationExpression

PrimaryNoNewArray:
  Literal
  ClassLiteral
  this
  TypeName . this
  ( Expression )
  ClassInstanceCreationExpression
  FieldAccess
  ArrayAccess
  MethodInvocation
  MethodReference
  switch ( Expression ) { {SwitchExpressionCase} }

SwitchExpressionCase:
  case Identifier [Identifiers] : return Expression ;

Identifiers:
  ( [Identifier {, Identifier}] )

ClassLiteral:
  TypeName {[ ]} . class
  NumericType {[ ]} . class
  boolean {[ ]} . class
  void . class

ClassInstanceCreationExpression:
  UnqualifiedClassInstanceCreationExpression
  ExpressionName . UnqualifiedClassInstanceCreationExpression
  Primary . UnqualifiedClassInstanceCreationExpression

UnqualifiedClassInstanceCreationExpression:
  new [TypeArguments] ClassOrInterfaceTypeToInstantiate ( [ArgumentList] ) [ClassBody]

ClassOrInterfaceTypeToInstantiate:
  {Annotation} Identifier {. {Annotation} Identifier} [TypeArgumentsOrDiamond]

ArrayCreationExpression:
  ArrayCreationExpressionWithoutInitializer
  ArrayCreationExpressionWithInitializer

ArrayCreationExpressionWithoutInitializer:
  new PrimitiveType DimExprs [Dims]
  new ClassOrInterfaceType DimExprs [Dims]

ArrayCreationExpressionWithInitializer:
  new PrimitiveType Dims ArrayInitializer
  new ClassOrInterfaceType Dims ArrayInitializer

DimExprs:
  DimExpr {DimExpr}

DimExpr:
  {Annotation} [ Expression ]

ArrayAccess:
  ExpressionName [ Expression ]
  PrimaryNoNewArray [ Expression ]
  ArrayCreationExpressionWithInitializer [ Expression ]

FieldAccess:
  Primary . Identifier
  super . Identifier
  TypeName . super . Identifier

MethodInvocation:
  MethodName ( [ArgumentList] )
  Typename . [TypeArguments] Identifier ( [ArgumentList] )
  ExpressionName . [TypeArguments] Identifier ( [ArgumentList] )
  Primary . [TypeArguments] Identifier ( [ArgumentList] )
  super . [TypeArguments] Identifier ( [ArgumentList] )
  TypeName . super . [TypeArguments] Identifier ( [ArgumentList] )

ArgumentList:
  Expression {, Expression}

Expression:
  LambdaExpression
  AssignmentExpression

AssignmentExpression:
  ConditionalExpression
  Assignment

Assignment:
  LeftHandSide AssignmentOperator Expression

LeftHandSide:
  ExpressionName
  FieldAccess
  ArrayAccess

AssignmentOperator:
  (one of)
  = *= /= %= += -= <<= >>= >>>= &= ^= |= 

ConditionalExpression:
  ConditionalOrExpression
  ConditionalOrExpression ? Expression : ConditionalExpression
  ConditionalOrExpression ? Expression : LambdaExpression

ConditionalOrExpression:
  ConditionalAndExpression
  ConditionalOrExpression || ConditionalAndExpression

ConditionalAndExpression:
  InclusiveOrExpression
  ConditionalAndExpression &&l; InclusiveOrExpression

InclusiveOrExpression:
  ExclusiveOrExpression
  InclusiveOrExpression | ExclusiveOrExpression

ExclusiveOrExpression:
  AndExpression
  ExclusiveOrExpression ^ AndExpression

AndExpression:
  EqualityExpression
  AndExpression & EqualityExpression

EqualityExpression:
  RelationalExpression
  EqualityExpression == RelationalExpression
  EqualityExpression != RelationalExpression

RelationalExpression:
  TruncatingExpression
  RelationalExpression < TruncatingExpression
  RelationalExpression > TruncatingExpression
  RelationalExpression <= TruncatingExpression
  RelationalExpression >= TruncatingExpression
  InstanceofExpression

InstanceofExpression:
  RelationalExpression instancof ReferenceType
  RelationalExpression instanceof Pattern

TruncatingExpression:
  ShiftExpression
  /*@ truncating @*/ PostfixExpression
  truncating PostfixExpression

ShiftExpression:
  AdditiveExpression
  ShiftExpression << AdditiveExpression
  ShiftExpression >> AdditiveExpression
  ShiftExpression >>> AdditiveExpression

AdditiveExpression:
  MultiplicativeExpression
  AdditiveExpression + MultiplicativeExpression
  AdditiveExpression - MultiplicativeExpression

MultiplicativeExpression:
  UnaryExpression
  MultiplicativeExpression * UnaryExpression
  MultiplicativeExpression / UnaryExpression
  MultiplicativeExpression % UnaryExpression

UnaryExpression:
  PreIncrementExpression
  PreDecrementExpression
  + UnaryExpression
  - UnaryExpression
  UnaryExpressionNotPlusMinus

PreIncrementExpression:
  ++ UnaryExpression

PreDecrementExpression:
  -- UnaryExpression

UnaryExpressionNotPlusMinus:
  PostfixExpression
  ~ UnaryExpression
  ! UnaryExpression
  CastExpression
  SwitchExpression

PostfixExpression:
  Primary
  ExpressionName [TypeArguments]
  PostIncrementExpression
  PostDecrementExpression

PostIncrementExpression:
  PostfixExpression ++

PostDecrementExpression:
  PostfixExpression --

CastExpression:
  ( PrimitiveType ) UnaryExpression
  ( ReferenceType {AdditionalBound} ) UnaryExpressionNotPlusMinus
  ( ReferenceType {AdditionalBound} ) LambdaExpression