VeriLib

Home / Code Info

View Code

Summary:

Filename or URL:

Language:

Actions:

Failed to verify the file. Unable to parse the verify result. MatrixStringOperations.dfy(14,17): Error: new can be applied only to class types (got seq)
   |
14 |     var parts := new seq();
   |                  ^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(37,18): Error: new can be applied only to class types (got seq>)
   |
37 |     var result := new seq>(rows.Length);
   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(39,23): Error: type seq does not have a member Length
   |
39 |     for i := 0 to rows.Length - 1 {
   |                   ^^^^^^^^^^^

MatrixStringOperations.dfy(41,22): Error: new can be applied only to class types (got seq)
   |
41 |         var rowSeq := new seq(row.Length);
   |                       ^^^^^^^^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(42,26): Error: type seq does not have a member Length
   |
42 |         for j := 0 to row.Length - 1 {
   |                       ^^^^^^^^^^

MatrixStringOperations.dfy(43,25): Error: unresolved identifier: Int
   |
43 |             rowSeq[j] := Int(row[j]);
   |                          ^^^

MatrixStringOperations.dfy(48,6): Error: RHS (of type array?) not assignable to LHS (of type seq>)
   |
48 |     m := result;
   |     ^^^^^^^^^^^^

MatrixStringOperations.dfy(43,19): Error: incorrect type for selection into ? (got int)
   |
43 |             rowSeq[j] := Int(row[j]);
   |                    ^

MatrixStringOperations.dfy(67,12): Error: expression is not allowed to invoke a method (matrixSum)
   |
67 |     ensures matrixSum(s1, s2) == res
   |             ^^^^^^^^^

MatrixStringOperations.dfy(67,21): Error: method call is not allowed to be used in an expression context (matrixSum)
   |
67 |     ensures matrixSum(s1, s2) == res
   |             ^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(80,29): Error: type of the receiver is not fully determined at this program point
   |
80 |             row := row + sum.ToString() + " ";
   |                          ^^^^^^^^^^^^

MatrixStringOperations.dfy(82,31): Error: type seq does not have a member Trim
   |
82 |         result := result + row.Trim() + "|"; // add row with separator
   |                            ^^^^^^^^

MatrixStringOperations.dfy(97,12): Error: expression is not allowed to invoke a method (matrixDifference)
   |
97 |     ensures matrixDifference(s1, s2) == res
   |             ^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(97,28): Error: method call is not allowed to be used in an expression context (matrixDifference)
   |
97 |     ensures matrixDifference(s1, s2) == res
   |             ^^^^^^^^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(110,30): Error: type of the receiver is not fully determined at this program point
    |
110 |             row := row + diff.ToString() + " ";
    |                          ^^^^^^^^^^^^^

MatrixStringOperations.dfy(130,12): Error: expression is not allowed to invoke a method (matrixProduct)
    |
130 |     ensures matrixProduct(s1, s2) == res
    |             ^^^^^^^^^^^^^

MatrixStringOperations.dfy(130,25): Error: method call is not allowed to be used in an expression context (matrixProduct)
    |
130 |     ensures matrixProduct(s1, s2) == res
    |             ^^^^^^^^^^^^^^^^^^^^^

MatrixStringOperations.dfy(147,29): Error: type int does not have a member ToString
    |
147 |             row := row + sum.ToString() + " ";
    |                          ^^^^^^^^^^^^

MatrixStringOperations.dfy(149,31): Error: type seq does not have a member Trim
    |
149 |         result := result + row.Trim() + "|"; // add row with separator
    |                            ^^^^^^^^

19 resolution/type errors detected in test.dfy

Description:

File:

Uploaded Date:

2025-05-01 13:03:19 UTC

Name	Verify	Status

Code:

method IndexOf(s: string, delimiter: string) returns (idx: int)
{
    var n := |s| - |delimiter| + 1;
    for i := 0 to n - 1 {
        if s[i..i + |delimiter|] == delimiter {
            return i;
        }
    }
    return -1; // Not found
}

method Split(s: string, delimiter: string) returns (result: seq<string>)
{
    var parts := new seq<string>();
    var startIdx := 0;
    var endIdx := IndexOf(s, delimiter);
    while endIdx != -1 {
        parts := parts + [s[startIdx..endIdx]];
    }
    parts := parts + [s[startIdx..]]; // add the last part
    result := parts;
}

predicate ValidMatrix(s: string)
{
    // All characters must be digits and matrices are properly formatted
    forall i | 0 <= i < |s| :: (s[i] == '0' || s[i] == '1' || s[i] == '2' || s[i] == '3' || s[i] == '4' || s[i] == '5' || s[i] == '6' || s[i] == '7' || s[i] == '8' || s[i] == '9' || s[i] == ' ' || s[i] == '|')
}

// ----------------------------------------------------
// Helper methods for matrix manipulation
// ----------------------------------------------------
method normalizeMatrix(s: string) returns (m: seq<seq<int>>)
    requires ValidMatrix(s)
{
    var rows := Split(s, "|");
    var result := new seq<seq<int>>(rows.Length);

    for i := 0 to rows.Length - 1 {
        var row := Split(rows[i], " ");
        var rowSeq := new seq<int>(row.Length);
        for j := 0 to row.Length - 1 {
            rowSeq[j] := Int(row[j]);
        }
        result[i] := rowSeq;
    }

    m := result;
}

// ----------------------------------------------------
// Reference methods for matrix operations
// ----------------------------------------------------
method matrixSum(s1: string, s2: string) returns (res: string)
{
    var m1 := normalizeMatrix(s1);
    var m2 := normalizeMatrix(s2);
    // Assuming matrices are of the same size, compute sum
}

// ----------------------------------------------------
// 1) add: string-based matrix addition
// ----------------------------------------------------
method add(s1: string, s2: string) returns (res: string)
    requires ValidMatrix(s1) && ValidMatrix(s2)
    ensures ValidMatrix(res)
    ensures matrixSum(s1, s2) == res
{
    var x := normalizeMatrix(s1);
    var y := normalizeMatrix(s2);

    var rows := |x|; // Assuming both matrices have the same number of rows
    var cols := |x[0]|; // Assuming both matrices have the same number of columns

    var result := "";
    for i := 0 to rows - 1 {
        var row := "";
        for j := 0 to cols - 1 {
            var sum := (x[i][j] + y[i][j]);
            row := row + sum.ToString() + " ";
        }
        result := result + row.Trim() + "|"; // add row with separator
    }

    res := result;
}

method matrixDifference(s1: string, s2: string) returns (res: string)
{
    var m1 := normalizeMatrix(s1);
    var m2 := normalizeMatrix(s2);
    // Assuming matrices are of the same size, compute difference
}
method sub(s1: string, s2: string) returns (res: string)
    requires ValidMatrix(s1) && ValidMatrix(s2)
    ensures ValidMatrix(res)
    ensures matrixDifference(s1, s2) == res
{
    var x := normalizeMatrix(s1);
    var y := normalizeMatrix(s2);

    var rows := |x|; // Assuming both matrices have the same number of rows
    var cols := |x[0]|; // Assuming both matrices have the same number of columns

    var result := "";
    for i := 0 to rows - 1 {
        var row := "";
        for j := 0 to cols - 1 {
            var diff := (x[i][j] - y[i][j]);
            row := row + diff.ToString() + " ";
        }
    }

    res := result;
}

method matrixProduct(s1: string, s2: string) returns (res: string)
{
    var m1 := normalizeMatrix(s1);
    var m2 := normalizeMatrix(s2);
    // Compute matrix multiplication
}

// ----------------------------------------------------
// 3) mul: string-based matrix multiplication
// ----------------------------------------------------
method mul(s1: string, s2: string) returns (res: string)
    requires ValidMatrix(s1) && ValidMatrix(s2)
    ensures ValidMatrix(res)
    ensures matrixProduct(s1, s2) == res
{
    var x := normalizeMatrix(s1);
    var y := normalizeMatrix(s2);

    var rows := |x|; // Number of rows of first matrix
    var cols := |y[0]|; // Number of columns of second matrix
    var innerDim := |x[0]|; // Inner dimension (should match between matrices)

    var result := "";
    for i := 0 to rows - 1 {
        var row := "";
        for j := 0 to cols - 1 {
            var sum := 0;
            for k := 0 to innerDim - 1 {
                sum := sum + x[i][k] * y[k][j];
            }
            row := row + sum.ToString() + " ";
        }
        result := result + row.Trim() + "|"; // add row with separator
    }

    res := result;
}
method Main() {
    print "Matrix Operations Example:\n";

    var a := "1 2 3|4 5 6";  // 2x3 matrix
    var b := "7 8 9|10 11 12";  // 2x3 matrix

    print "Matrix A:\n", a, "\n";
    print "Matrix B:\n", b, "\n";

    var s := add(a, b);
    print "A + B = ", s, "\n";

    var d := sub(b, a);
    print "B - A = ", d, "\n";

    var m := mul(a, b);
    print "A * B = ", m, "\n";
}

View Code

Dependency Graph: Preview

File Explorer:

View Code

Delete Confirmation

Confirmation Required

Confirmation Required

Confirmation Required

Confirmation Required

Dependency Graph: Preview

File Explorer: