Моделирование вектора / массива фиксированного размера в Boogie

Question

Я пытаюсь моделировать векторы фиксированной длины в буги. Каждый вектор с разным размером должен быть другого типа.

Я попробовал два подхода, но у обоих есть особая проблема.

Подход 1: Тип псевдонимов

Определите псевдоним типа и некоторые аксиомы, которые описывают длину для псевдонима типа. Однако, поскольку создается только псевдоним, а не новый тип, аксиомы действительны для всех псевдонимов. Следовательно, мы получаем противоречивые аксиомы.

function length(x: [int]real) returns (n: int);

type Vector3 = [int]real;
axiom (forall x: Vector3 :: length(x) == 3);

type Vector5 = [int]real;
// The following axiom conflicts with the previous one.
axiom (forall x: Vector5 :: length(x) == 5); 

procedure impl1();
implementation impl1()
{
  var v1: Vector3;
  var v2: Vector5;

    v1[0] := 1.0;
    v1[0] := 2.0;
    v1[0] := 3.0;

    assert length(v1) == 3;
    assert length(v2) == 5;
    assert length(v1) == 999; // Must fail but it doesn't.
}

Подход 2: свежие виды

Здесь мы создаем новый тип для каждого вектора фиксированной длины с маркером "Dim3", чтобы сделать его уникальным. Длина описывается с использованием аксиомы. Проблема здесь в том, что я не знаю, как получить доступ / назначить карту, которая является частью этого типа.

function length<D>(x: Vector D [int]real) returns (n: int);

type Vector alpha beta;

type Dim1;
type Dim2;
type Dim3;
type Dim4;
type Dim5;

type Vector3 = Vector Dim3 [int]real;
axiom (forall x: Vector3 :: length(x) == 3);

type Vector5 = Vector Dim5 [int]real;
axiom (forall x: Vector5 :: length(x) == 5);


procedure impl1();
implementation impl1()
{
  var v1: Vector3;
  var v2: Vector5;

    v1[0] := 1.0; // Invalid boogie code: 'Error: map assignment applied to a non-map'
    v1[0] := 2.0;
    v1[0] := 3.0;

    assert length(v1) == 3;
    assert length(v2) == 5; 
}

Я был бы рад, если бы кто-то указал мне правильное направление!