Groups | Search | Server Info | Login | Register

Groups > de.alt.folklore.computer > #51021

Re: Chatbot-Demo

Show all headers | View raw

ram@zedat.fu-berlin.de (Stefan Ram) schrieb oder zitierte:
>Nun wird es spannend: Wird der Chatbot die verwendeten Fachbegriffe
>richtig verstehen und ein vollständiges Computer-Programm selbständig
>schreiben können wie ein Mensch??

  Nun, hier ist die Antwort des Chatbots:

Formale Spezifikation

"S(lst)" die Menge aller "str"-Objekte, die in "lst"
(rekursiv) enthalten sind.

Dann gilt:
"length(lst) = sum(len(s) for s in S(lst))"

Kontrakt

Vorbedingung:

Das Argument "lst" ist entweder ein "str"-Objekt oder eine
Liste, deren Elemente wiederum entweder "str"-Objekte oder
Listen gleicher Struktur sind.

Es gibt keine anderen Typen in der Struktur.

Nachbedingung:

Das Ergebnis ist die Summe der Längen aller enthaltenen
"str"-Objekte in beliebiger Tiefe.

Implementation (Python 3.13)

from typing import Union, List

def length(lst: Union[str, List["lst"]]) -> int:
    """
    Berechnet die Summe der Längen aller str-Objekte in einer 
    (rekursiv) verschachtelten Liste.

    :param lst: Ein str-Objekt oder eine Liste, deren Elemente 
                entweder str oder Listen gleicher Struktur sind.
    :type lst: Union[str, List]
    :return: Die Summe der Längen aller enthaltenen str-Objekte.
    :rtype: int

    Schwächste Vorbedingung:
        lst ist entweder ein str-Objekt oder eine Liste, die 
        nur str-Objekte oder Listen gleicher Struktur enthält.

    Schleifeninvariante:
        Nach jeder Iteration über ein Element der Liste ist 
        die Zwischensumme die korrekte Summe der Längen aller 
        bisher betrachteten Elemente (rekursiv).
    """
    if isinstance(lst, str):
        # Basisfall: lst ist ein str-Objekt, dessen Länge gezählt wird.
        return len(lst)
    else:
        # Rekursiver Fall: lst ist eine Liste, summiere rekursiv über 
        # alle Elemente.
        return sum(length(element) for element in lst)

Beweis der Korrektheit und Terminierung

Korrektheit

Induktionsanfang (Basisfall):

Wenn "lst" ein "str"-Objekt ist, liefert die Funktion
"len(lst)". Dies ist genau die Länge des einzigen enthaltenen
Strings, also korrekt.

Angenommen, für alle Listen der Tiefe ≤ n liefert die Funktion
das korrekte Ergebnis.

Für eine Liste der Tiefe n+1:

- Die Funktion ruft sich rekursiv für jedes Element auf.

- Nach Induktionsannahme liefert jeder rekursive Aufruf die
  korrekte Summe für das jeweilige Element.

- Die Summe aller rekursiven Ergebnisse ist somit die
  Gesamtsumme aller enthaltenen Strings.

Schleifeninvariante:
Nach jeder Iteration (im Generatorausdruck) ist die
Zwischensumme die korrekte Summe der Längen aller bisher
betrachteten Elemente.

Terminierung

- Die Rekursion terminiert, da jede Liste endlich ist und die
  Rekursionstiefe mit jeder Ebene um 1 abnimmt.

- Der Basisfall ("str") ist immer endlich, da Strings nicht
  weiter rekursiv aufgelöst werden.

- Es gibt keine zyklischen Strukturen, da dies laut
  Vorbedingung ausgeschlossen ist.

  So weit der Chatbot. Aber wird das bewiesene Programm auch alle Tests
  bestehen? Dies weiß kein Mensch! Aber nur bis morgen, denn dann werde
  ich hier auch noch die Ergebnisse der Tests veröffentlichen . . .

  Also, lies morgen weiter, um zu sehen, was die Tests ergaben!

Back to de.alt.folklore.computer | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-06-29 13:29 +0000
  Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-06-29 13:37 +0000
    Re: Chatbot-Demo Ulf Kutzner <user2991@newsgrouper.org.invalid> - 2025-06-29 13:47 +0000
      Re: Chatbot-Demo Marc Haber <mh+usenetspam1118@zugschl.us> - 2025-06-30 10:22 +0200
        Re: Chatbot-Demo Ulf Kutzner <user2991@newsgrouper.org.invalid> - 2025-06-30 08:32 +0000
    Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-06-30 12:15 +0000
      Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-07-01 10:22 +0000
        Re: Chatbot-Demo michaelnoeusenet@mac.com (Michael Noe) - 2025-07-01 21:31 +0200
        Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-07-02 12:24 +0000
          Re: Chatbot-Demo Thomas Koenig <tkoenig@netcologne.de> - 2025-07-02 16:56 +0000
            Re: Chatbot-Demo michaelnoeusenet@mac.com (Michael Noe) - 2025-07-03 18:00 +0200
              Re: Chatbot-Demo mlelstv@serpens.de (Michael van Elst) - 2025-07-03 16:37 +0000
                Re: Chatbot-Demo michaelnoeusenet@mac.com (Michael Noe) - 2025-07-03 22:07 +0200
          Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-07-03 13:00 +0000
            Re: Chatbot-Demo ram@zedat.fu-berlin.de (Stefan Ram) - 2025-07-04 14:08 +0000
              42 (was: Chatbot-Demo) michaelnoeusenet@mac.com (Michael Noe) - 2025-07-05 17:48 +0200
  Nicht auch noch $HIER! (was: Chatbot-Demo) Kay Martinen <usenet@martinen.de> - 2025-06-29 16:47 +0200
    Re: Nicht auch noch $HIER! michaelnoeusenet@mac.com (Michael Noe) - 2025-06-29 17:41 +0200
      Re: Nicht auch noch $HIER! Thomas Koenig <tkoenig@netcologne.de> - 2025-06-29 20:41 +0000
    Re: Nicht auch noch $HIER! Andreas Bockelmann <xotzil@gmx.de> - 2025-07-02 08:33 +0200

csiph-web