Äquivalenz zweier Programme



  • Hallo zusammen,

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    VG, freakC++



  • Das wird auf das Halteproblem hinauslaufen, geht also nicht. Außer in irgendwelchen klar definierten Sonderfällen.



  • Anzahl der Zeilen Code.



  • Beweisen? Könntest du höchstens wenn du den Graphen des Algorithmus auf elementare Basisoperationen herunterbrichst, vereinfachst und für diesen zeigst dass er isomorph ist.

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.



  • Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.



  • Troll der Kenner schrieb:

    Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.

    Ethon hat "endliche Eingabemenge" geschrieben und das funktioniert. Bei einem Programm, dass endlich viele Eingaben hat, kann man alle durchprobieren und so unter der Annahme, dass genug Speicher zur verfuegung steht, auf Gleichheit ueberpruefen.



  • Marthog schrieb:

    Ethon hat "endliche Eingabemenge" geschrieben und das funktioniert. Bei einem Programm, dass endlich viele Eingaben hat, kann man alle durchprobieren und so unter der Annahme, dass genug Speicher zur verfuegung steht, auf Gleichheit ueberpruefen.

    nur unter der Voraussetzung, dass beide Programme für alle Eingaben anhalten ➡ Halteproblem, wie schon erwähnt



  • Marthog schrieb:

    Ethon hat "endliche Eingabemenge" geschrieben und das funktioniert. Bei einem Programm, dass endlich viele Eingaben hat, kann man alle durchprobieren und so unter der Annahme, dass genug Speicher zur verfuegung steht, auf Gleichheit ueberpruefen.

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.



  • freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡



  • Troll der Kenner schrieb:

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.



  • Marthog schrieb:

    Troll der Kenner schrieb:

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.

    Also nochmal langsam. Nur weil ich von einem Programm die Ausgabe haben will, terminiert dieses automatisch? Das ist ja nett 😉



  • Marthog schrieb:

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.

    der threadersteller fragte aber wie man zwei programme vergleichen kann. wie zwei shorts miteinander verglichen werden sollte jedem hier klar sein.

    akzeptable zeit? schwammiger begriff. mein programm, das mit brute-force prueft, ob 2^127-1 eine primzahl ist, ist meiner meinung nach ebenso akzeptabel wie dasjenige, das den lucas-lehmer-test verwendet. wenn du keine fixe grenze fuer "akzeptabel" angeben kannst, ist deine aussage nichtig. wenn du eine angeben kannst, dann zeige ich dir mit dem heap-paradoxon, dass diese sinnlos und willkuerlich ist.



  • cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    doch nicht so easy, equal hat als dritten parameter first der zweiten sequenz, nicht last.



  • Da müsste man definieren was äquivalent ist.
    Wenn damit gemeint ist dass ein bestimmtes Eingabe-Tupel ein gewisses Ausgabe-Tupel erzeugt dann wird das mit dem Beweis nichts, siehe Halteproblem. Kann sicherlich ein Problem so verhunzen dass es in O(n!) anstatt O(n) läuft.



  • cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    Auf endlichen Eingabemengen gibt dieser Code bei mir das gleiche Resultat wie das Programm

    return reinretpret_cast<std::vector*>(61262)->empty();
    

    Sind die beiden Programme jetzt gleich oder war das jetzt Zufall?



  • equipotential schrieb:

    cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    Auf endlichen Eingabemengen gibt dieser Code bei mir das gleiche Resultat wie das Programm

    return reinretpret_cast<std::vector*>(61262)->empty();
    

    Sind die beiden Programme jetzt gleich oder war das jetzt Zufall?

    Auf was willst du hinaus? Er hat nur den Quelltext auf Äquivalenz geprüft und das ist definitiv eine valide Möglichkeit Algorithmen auf Äquivalenz zu prüfen.

    Troll der Kenner schrieb:

    Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.

    Theoretisch ja, praktisch aber mMn. nach ausreichend.



  • Ethon schrieb:

    Beweisen? Könntest du höchstens wenn du den Graphen des Algorithmus auf elementare Basisoperationen herunterbrichst, vereinfachst und für diesen zeigst dass er isomorph ist.

    funktioniert auch nur begrenzt (sofern man davon ausgeht dass computer fuer mathematische beweise nicht geeignet sind, was sie derzeit definitiv nicht sind). beispiel:

    //programm 1:
    double pi_square_div_6() //gibt pi^2/6 aus
    {
        //approximation mit einem big_float und summation der kehrwerte der quadrate der natuerlichen zahlen
    }
    //programm 2:
    double pi_square_div_6()
    {
        //monte-carlo-apporximation von pi mit einem zaehler + aes als zufallsquelle, dann / 6
    }
    //programm 3:
    double pi_square_div_6()
    {
        //numerische approximation an zeta(2)
    }
    

    dass die vom compiler generierten assembler-instruktionen in irgendeiner weise maschinell beweisbar zusammenhaengen wage ich sehr zu bezweifeln.

    fuer simple aufgaben ist diese herangehensweise allerdings interessant, da fallen mir spontan spannende faelle fuer rekursiv / iterativ ein (mit zyklischen graphen / flussdiagrammen). maschinell iterativen c++-code in eine rekursive form bringen? koestlich!



  • Ethon schrieb:

    Auf was willst du hinaus? Er hat nur den Quelltext auf Äquivalenz geprüft und das ist definitiv eine valide Möglichkeit Algorithmen auf Äquivalenz zu prüfen.

    Sein Code war UB, meiner auch.
    Ich wollte hinaus, dass nur weil der Code einmal etwas ausgibt, er das nächste mal etwas völlig anderes ausgeben kann, warum auch immer (UB, rand(), externe Abhängigkeit, etc.).

    Ethon schrieb:

    Troll der Kenner schrieb:

    Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.

    Theoretisch ja, praktisch aber mMn. nach ausreichend.

    Man kann mit dieser Methode maximal beweisen, dass sie nicht gleich sind (wenn sie terminieren ein unterschiedliches Resultat ergeben), noch dass sie gleich sind (selbst wenn sie das gleiche Resultat ausspucken, sie könnten mit Wahrscheinlichkeit von 10^-80 ein falsches Resultat liefern).


  • Mod

    equipotential schrieb:

    Man kann mit dieser Methode maximal beweisen, dass sie nicht gleich sind (wenn sie terminieren ein unterschiedliches Resultat ergeben), noch dass sie gleich sind (selbst wenn sie das gleiche Resultat ausspucken, sie könnten mit Wahrscheinlichkeit von 10^-80 ein falsches Resultat liefern).

    Wenn wir vom theoretischen Idealbild ausgehen, dann ist die Maschine streng deterministisch. Diese Faktoren, die in diesem Beispiel dafuer sorgen, dass manchmal etwas anderes rauskommen kann, sind ein versteckter Teil der Eingabemenge.



  • Ethon schrieb:

    Beweisen? Könntest du höchstens wenn du den Graphen des Algorithmus auf elementare Basisoperationen herunterbrichst, vereinfachst und für diesen zeigst dass er isomorph ist.

    Klingt ja interessant. Was ist denn der Graph eines Algorithmus? Und auf welchen Äquivalenzbegriff bezieht sich das?


Anmelden zum Antworten