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";

}