Cost Aware Dafny for Visual Studio Code

This extension bundles the Dafny Cost-Aware plugin (DafnyCostAwarePlugin.dll) and the required Dafny library (MathR0.doo) so you can use cost-aware specifications in Dafny through VS Code.

Cost-Aware Specifications (Plugin Overview)

The plugin adds cost-related specification annotations to Dafny methods using ensures attributes.

The main attribute is {:count ...}, wich declares a named cost counter with an associated cost model described by a list of criterias.

Conceptually, these annotations let you express quantitative statements about program behaivour such as:

• "This method performs at most N writes"
• "This method performs at least N + operations"
• "This method performs exactly N calls to Foo"

Adding {:count ...} attributes to ensures

The full shape of a cost-aware specification is:

ensures {:count <counterRef> [, <criteriaArg>] [, <optionsArg>]} <counterRef> <cmp> <expr>

where <cmp> is one of: ==, <=, >=

Examples:

ensures {:count t} t <= 10.0
ensures {:count t, "write:x"} t == 2.0
ensures {:count t, ["write:x", "op:(+)"], "strict"} t <= 4.0

This declares a counter reference (t) and constrains it in the same ensures formula.

Filtered counts by criteria

You can restrict what the counter counts by adding one criterion string or a list of criterion strings:

ensures {:count t, "write:x"} t == 2.0
ensures {:count t, ["write:x", "op:(+)"]} t == 4.0

Defaults:

• If no criteria are provided, the plugin uses its default "count all supported core events" behavior
• [] or "" means count nothing (free counter)
• "*" means the universal core set (write, read, call, arithmetic op, relational rel, alloc) and intentionally excludes loop, entry, and mark unless explicitly requested

Supported Criteria

The plugin parser supports the following criteria forms.

Write / Read

• write:_ (any write)
• write:x (writes to variable x)
• write:a[0], write:a[_], write:a[_,_], write:a[0][_]
• read:_, read:x, read:a[_], etc.

Example:

method M(a: array<int>) returns (t: real)
  ensures {:count t, "write:a[_]"} t >= 1.0
{
  a[0] := 10;
  t := 1.0;
}

Arithmetic operations (op:)

Format:

• op:(+)
• op:(-)
• op:(*)
• op:(/)
• op:(_) (any arithmetic op)
• More specific operand patterns are also supported, e.g. op:x (+) 1

Example:

ensures {:count t, "op:(+)"} t >= 0.0

Relational operations (rel:)

Format:

• rel:(<)
• rel:(<=)
• rel:(>)
• rel:(>=)
• rel:(==)
• rel:(!=)
• rel:(_) (any supported relational op)

Example:

ensures {:count t, "rel:(<=)"} t >= 0.0

Calls

• call:Foo (calls to method/function Foo)
• call:_ (any call)

Example:

ensures {:count t, "call:Helper"} t <= 3.0

Allocations

• alloc:_ (any allocation)
• alloc:array1, alloc:array2 (any rank-1 / rank-2 array allocation)
• alloc:int
• alloc:int[,]
• alloc:array<char>

Example:

ensures {:count t, "alloc:array1"} t >= 0.0

Loop / Entry / Mark

• loop
• entry
• mark:<name> or mark:_

These are not included by "*" and must be requested explicitly.

Example:

ensures {:count t, ["*", "loop"]} t >= 0.0

Options (third attribute argument)

{:count ...} accepts an optional third argument: a list of option strings.

Recognized options include:

• strict
• union (or alias for non-additive behavior: non-additive, nonadditive, or)

Example:

ensures {:count t, "call:Helper", "strict"} t <= 2.0

Notes

• This extension's job is to bundle the plugin and configure Dafny VS Code to load it.
• For extension implementation details, packaging, and repository-oriented docs, see: https://github.com/dafny-cost-aware/ide-vscode
• For plugin source and tests, see: https://github.com/dafny-cost-aware/plugin