this post was submitted on 10 May 2024
2 points (75.0% liked)

Formal Methods

165 readers
3 users here now

founded 1 year ago
MODERATORS
 

Context: Dafny is a programming language with a built-in SMT solver that can encode formally-checked statements (e.g. preconditions, postconditions, assertions).

Dafny has features of most programming languages; for example, covariant/contravariant/"non-variant" (invariant) type parameters. But in order to keep said verification sound and decidable in reasonable time, these features have extra restrictions and other complexities.

This article explains that there are 2 more "variance modes", because the of "covariant" and "invariant" variances may be "cardinality-preserving" or "not cardinality-preserving".

// Most "traditional" languages have 3 variances
type Foo<
    +CovariantParameter,
    NonVariantParameter,
    -ContravariantParameter>
// Dafny has 5
type Bar<
    +CovariantCardinalityPreservingParameter, 
    NonVariantCardinalityPreservingParameter,
    -ContravariantParameter, 
    *CovariantNonCardinalityPreservingParameter, 
    !NonVariantNonCardinalityPreservingParameter>
no comments (yet)
sorted by: hot top controversial new old
there doesn't seem to be anything here