Search results

assigns clause default to \everything, contrary to the OpenJML.org tutorial

Status: Open.

#938 In OpenJML/OpenJML;

· caiovpsilveira opened on Jan 4, 2026

int[][] clone fails for jagged, nullable arrays

Status: Open.

#937 In OpenJML/OpenJML;

· caiovpsilveira opened on Jan 2, 2026

Enhancement: add multiset predicate to OpenJML

Status: Open.

#936 In OpenJML/OpenJML;

· caiovpsilveira opened on Jan 2, 2026

'super' in specs not translated correctly

Status: Open.

#932 In OpenJML/OpenJML;

· davidcok opened on Dec 22, 2025

Specs for non-overloaded methods

Status: Open.

#931 In OpenJML/OpenJML;

· davidcok opened on Dec 18, 2025

Termination of model methods

Status: Open.

#930 In OpenJML/OpenJML;

· davidcok opened on Dec 18, 2025

Verifying SpecPure

Status: Open.

#929 In OpenJML/OpenJML;

· davidcok opened on Dec 18, 2025

RAC needs access functions for fields marked as spec_public or spec_protected

Status: Open.

#927 In OpenJML/OpenJML;

· davidcok opened on Dec 13, 2025

Use maps clauses to avoid the 'assigns \everything' in AutoCloseable

Status: Open.

#926 In OpenJML/OpenJML;

· davidcok opened on Dec 12, 2025

Implement invariants for loops having conditions with side-effects

Status: Open.

#924 In OpenJML/OpenJML;

· davidcok opened on Dec 11, 2025

Implement conversions from BigDecimal to and from \real

Status: Open.

#923 In OpenJML/OpenJML;

· davidcok opened on Dec 11, 2025

Matrix assumptions in gitbug883 that should not be needed

Status: Open.

#921 In OpenJML/OpenJML;

· davidcok opened on Dec 6, 2025