def multiply(a: int, b: int) -> int:
    x, y, p = a, b, 0
    # Die Schleifeninvariante gilt vor der Schleife
    assert (x * y) + p == a * b
    while x > 0:
        # Die Schleifeninvariante gilt an jedem Schleifenanfang
        assert (x * y) + p == a * b
        p = p + y
        # Zwischendrin muss diese nicht gelten
        x = x - 1
        # Die Schleifeninvariante muss am Ende jedes Durchlaufs gelten
        assert (x * y) + p == a * b
    # Die Schleifeninvariante muss ganz am Ende gelten
    assert (x * y) + p == a * b
    return p


if __name__ == "__main__":
    assert multiply(3, 4) == 12
    assert multiply(0, 1) == 0
    assert multiply(1000, 0) == 0
    assert multiply(100, 1000) == 100000
