design by contract mit compilerprüfung durch findbugs

[frankmusolf]

habe neulich entdeckt, dass findbugs die möglichkeit bietet, mit
annotations quasi design by contract bedingungen zu formulieren.

man bindet einfach die annotations.jar aus findbugs in sein projekt ein
und kann nun z.b. schreiben:

@NonNull String a(@NonNull String b)
{
return "abc";
}

die methode a darf nun nicht mit einem null-parameter aufgerufen
werden.
wenn man diese methode nun mit b = null aufruft, erzeugt findbugs nach
der compilierung eine fehlermeldung. also nicht erst zur laufzeit,
sondern schon während des entwickelns. auch wenn die methode anstatt
"abc" aus irgendeinem grund null zurückgeben würde, schimpft findbugs
sofort und ich sehe in eclipse gleich eine warnung.

es sind noch eine ganze menge mehr annotations möglich, z.b.
@CheckForReturn zum vorgeben, dass der rückkehrwert einer funktion
nicht ignoriert werden darf.

eine ähnliche technik gibt es wohl auch bei intellij. nur mit der
findbugs-lösung geht es auch in eclipse.

viel spass beim ausprobieren
frank

[Stefan Ram]

Post by frankmusolf
eine ähnliche technik gibt es wohl auch bei intellij. nur mit der
findbugs-lösung geht es auch in eclipse.

Siehe auch:

http://secure.ucd.ie/products/opensource/ESCJava2/

[Frank Buss]

Post by Stefan Ram

Post by frankmusolf
eine ähnliche technik gibt es wohl auch bei intellij. nur mit der
findbugs-lösung geht es auch in eclipse.

http://secure.ucd.ie/products/opensource/ESCJava2/

Sowas meinte ich. Sieht doch bedeutend mächtiger aus.

[Daniel Thoma]

Hallo Frank,

Post by Frank Buss
Sowas meinte ich. Sieht doch bedeutend mächtiger aus.

Erstmal ja, aber wenn man sich das detaillierter ansieht, sieht man,
dass auch da nur mit Wasser gekocht wird:
In
http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html
Appendix A wird kurz erläutert, was sie tun.

Sie basteln aus dem Programm wohl erstmal einen vereinfachten
Zwischencode und daraus eine logische Formel (vermutlich
prädikatenlogische). Da setzen sie dann einen Theorem-Prover drauf an.
Wenn der kein Ergebnis liefert, weil er zu lange braucht (im Falle von
Prädikatenlogik terminiert er ja sowieso u.U. nicht) dann geben sie
einfach keine Warnung aus. Schon bei der Umwandlung in die logische
Formel verlieren sie wohl ein Teil der Programmsemantik.

Dieses Tool findet also sicher den ein oder anderen Fehler, es
garantiert aber nicht die Abwesenheit von Fehlern. Außerdem dürfte es
auch Warnungen ausgeben, wenn gar keine Fehler vorliegen.

Im Allgemeinen ist es unentscheidbar, ob ein Programm korrekt ist oder
auch bloß bestimmte Eigenschaften erfüllt. Auch das Hoare-Kalkül enthält
nicht-automatisierbare Schritte und hilft da nicht weiter.
Solche Bedingungen, wie dass bestimmte Variablen nicht null sein dürfen,
lassen sich allerdings recht einfach durch Typsysteme und statische
Programmanalysen sicher stellen. Diese Verfahren sehen zwar auch Fehler
an Stellen, wo keine sind, aber damit kann man bei so einfachen
Bedingungen normalerweise leben.

So bald irgend welche logischen Formeln oder arithmetischen Ausdrücke
mit ins Spiel kommen, klappt das nicht mehr. Dann wird das alles extrem
Aufwendig und ist nicht mehr vollständig automatisierbar. So weit ich
weiß, sind Ansätze in dem Bereich bislang höchstens für Spezialsoftware
(Motorsteuerung o.ä.) und Hardware sinnvoll einsetzbar.

Grüße

Daniel Thoma

[Stefan Ram]

Post by Daniel Thoma
http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html
Appendix A wird kurz erläutert, was sie tun.

Diese ESC-Version kommt mit Typparametern ab Java 1.5 nicht
zurecht. (Eine neuere ist wohl irgendwo in Arbeit.)

FindBugs läuft jetzt nach einigen Startschwierigkeiten unter
einer alten Windows-Version und auf einem alten Rechner mit
geringer Leistung unter Dolphin.

Es ist ganz gut darin, daß es nicht so viele Meldungen
produziert, sondern versucht, sich auf einige wenige Hinweise
zu konzentrieren. Die GUI erleichtert die Anwendung für
Ungeübte.

An einer Stelle habe ich extra geschrieben

return new java.lang.String( string );

um eine Referenz auf eine Teilkette aufzulösen, damit der
Speicherbereiniger die enthaltende Kette dann auch freigeben
kann. FindBugs meint, ich solle das durch

return string;

ersetzen.

Es ist ganz nett, aber die meisten Fehler sind nicht so
schlimme Feinheiten, die für meine Projektstufe noch zu fein
sind. Da ich den Code noch öfter im Groben umschreibe, lohnt
es sich noch nicht auf diesem Niveau zu arbeiten.

[frankmusolf]

natürlich kann auch dieses tool keine wunderdinge vollbringen. unter
den ganzen ansätzen, die ich bisher bzgl. design by contract für java
gesehen habe, gefällt mir dieser aber am besten.

kein extra compiler, kein precompiler, einfach normal in eclipse
entwickeln und ich bekomme zur compile-zeit contract-verletzungen
geliefert. und in der regel funktioniert dies doch auch ganz gut.

mit gehörig durcheinander gewürfelten if's und return's hab ich die
null-reference-prüfung von eclipse auch schon zu einer falschen
aussage verführen können. trotzdem ist diese prüfung toll und ich
bin dankbar, dass es sie gibt.

[Frank Buss]

Post by frankmusolf
die methode a darf nun nicht mit einem null-parameter aufgerufen
werden.
wenn man diese methode nun mit b = null aufruft, erzeugt findbugs nach
der compilierung eine fehlermeldung. also nicht erst zur laufzeit,
sondern schon während des entwickelns.

Das ist ja ganz nett, aber kann es auch solche Zusicherungen geben, wie daß
eine Variable nach Verlassen der Methode einen bestimmten Wert hat, den man
per Formel angeben kann? Spark scheint das, und mehr, seit 20 Jahren zu
können:

http://www.praxis-his.com/sparkada/pdfs/sampler_final.pdf

Das beweist also zur Compilierzeit, daß der Code die entsprechenden
Nachbedingungen erfüllt. Wie gut es ist, weiß ich allerdings nicht, aber
ich sehe keinen Grund, warum nicht ein Compiler auch automatisch z.B. das
Hoare Kalkül anwenden können sollte, auch für Java.

http://www.pst.informatik.uni-muenchen.de/lehre/SS06/infoII/zentralfolien/kw19_hoare_fibonacci.pdf

[Gerd K.]

Hallo Frank!

Post by Frank Buss
Das beweist also zur Compilierzeit, daß der Code die entsprechenden
Nachbedingungen erfüllt. Wie gut es ist, weiß ich allerdings nicht, aber
ich sehe keinen Grund, warum nicht ein Compiler auch automatisch z.B. das
Hoare Kalkül anwenden können sollte, auch für Java.

Das scheitert schon alleine daran, dass es (noch?) keine formale
Semantik von Java gibt, d.h. keine formale Semantikdefinition einer
jeden Java-Anweisung. Das Definieren einer solchen Semantik ist
aktueller Forschungsgegenstand der Informatik.

Weiter kann das i.A. nicht funktionieren,da das Finden von für den
Beweis
"geeigneter" Schleifeninvarianten nicht berechenbar ist.

Grüße,
Gerd

[Stefan Ram]

Post by Gerd K.
Weiter kann das i.A. nicht funktionieren,da das Finden von für
den Beweis "geeigneter" Schleifeninvarianten nicht berechenbar
ist.

Es gibt allerdins Heuristiken, wie

http://pag.csail.mit.edu/daikon/

[Gerd K.]

Post by Stefan Ram

Post by Gerd K.
Weiter kann das i.A. nicht funktionieren,da das Finden von für
den Beweis "geeigneter" Schleifeninvarianten nicht berechenbar
ist.

Es gibt allerdins Heuristiken, wie
http://pag.csail.mit.edu/daikon/

Ja, aber das nützt so gut wie gar nichts *g*

Man sollte bei der Diskussion die verschiedenen
Arten von Schleifeninvarianten unterscheiden:
Triviale: true, im Hoare Kalkül auch false
Semantikbeschreibende Invarianten: Sagen etwas über die Semantik
der Schleife aus
"Geeignete" Invarianten: Mit diesen gelingt der zu führende
Beweis.

Die Schwierigkeit ist das Finden von geeigneten Invarianten,
denn die Tatsache, dass eine Invariante semantikbeschreibend ist,
ist weder notwendig noch hinreichend für die Geeignetheit.

Vereinfacht gesprochen muss die zu findende Invariante den
"Verifikations-Weg" von der Nachbedingung über die Schleife hin zur
Vorbedingung erlauben. Und dabei nutzten Heuristiken wenig, da
z.B. die obige "lediglich" Vermutungen aus den Variablenwerten
zur Laufzeit ableitet und eine Vor- bzw. Nachbedingung gar nicht
berücksichtigt.

Aber für java ist die ganze Diskussion eh sinnlos, solange die
formale Semantik der Sprache noch nicht definiert ist. ;-)

Grüße!
Gerd

[Hubert Schmid]

Post by Gerd K.
Das scheitert schon alleine daran, dass es (noch?) keine formale
Semantik von Java gibt, d.h. keine formale Semantikdefinition einer
jeden Java-Anweisung. Das Definieren einer solchen Semantik ist
aktueller Forschungsgegenstand der Informatik.

AFAIK existiert eine formale Semantik mit ASMs von Robert Stärk. Dazu
gibt es auch ein Buch: "Java and the Java Virtual Machine: Definition,
Verification, Validation"

[Gerd K.]

Hallo!

Post by Gerd K.
Das scheitert schon alleine daran, dass es (noch?) keine formale
Semantik von Java gibt, d.h. keine formale Semantikdefinition einer
jeden Java-Anweisung. Das Definieren einer solchen Semantik ist
aktueller Forschungsgegenstand der Informatik.

AFAIK existiert eine formale Semantik mit ASMs von Robert Stärk. Dazu
gibt es auch ein Buch: "Java and the Java Virtual Machine: Definition,
Verification, Validation"

Die dort vorgestellte Semantikdefinition mag zwar zur
bytecode-Verifikation ausreichen, aber es ist keine formale
Sematikdefiniton die mächtig genug wäre, um die
Verifikation zu ermöglichen, über die hier diskutiert wurde,
nämlich der mathematische Nachweis, dass ein java-Programm(teil)
sich gemäß einer in Vor- und Nachbedingung angegebenen Spezifikation
verhält. Das ist eine ganz andere Qualität als das Überprüfen auf
Bytecodeebene, ob Objekte, Register initialisiert, ob es Stapel-
überlauf, ob es Typkorrektheit gibt etc.

Grüße!

[Ingo Menger]

Post by Gerd K.
Hallo!

Post by Gerd K.
Das scheitert schon alleine daran, dass es (noch?) keine formale
Semantik von Java gibt, d.h. keine formale Semantikdefinition einer
jeden Java-Anweisung. Das Definieren einer solchen Semantik ist
aktueller Forschungsgegenstand der Informatik.

AFAIK existiert eine formale Semantik mit ASMs von Robert Stärk. Dazu
gibt es auch ein Buch: "Java and the Java Virtual Machine: Definition,
Verification, Validation"

Die dort vorgestellte Semantikdefinition mag zwar zur
bytecode-Verifikation ausreichen, aber es ist keine formale
Sematikdefiniton die mächtig genug wäre, um die
Verifikation zu ermöglichen, über die hier diskutiert wurde,
nämlich der mathematische Nachweis, dass ein java-Programm(teil)
sich gemäß einer in Vor- und Nachbedingung angegebenen Spezifikation
verhält. Das ist eine ganz andere Qualität als das Überprüfen auf
Bytecodeebene, ob Objekte, Register initialisiert, ob es Stapel-
überlauf, ob es Typkorrektheit gibt etc.

Mal eine theoretische Frage in dem Zusammenhang: Wäre es denn nicht
denkbar, die Prüfungen anhand des generierten Bytecodes zu machen,
denn letzterer hat doch eine feststehende Semantik.
(Praktisch wär das natürlich fast wertlos, da den Beweis, daß eine
Nachbedingung verletzt oder eine Vorbedingung nicht eingehalten ist
kaum einer lesen und verstehen könnte.)

[Gerd K.]

Post by Ingo Menger
Mal eine theoretische Frage in dem Zusammenhang: Wäre es denn nicht
denkbar, die Prüfungen anhand des generierten Bytecodes zu machen,
denn letzterer hat doch eine feststehende Semantik.

Das scheitert an einigen Punkten:

- GOTOs ;-)
Programme mit unbedingten Sprüngen sind so gut wie gar nicht
(gegen eine Spezifikaton) zu verifizieren

- Die Vor- und Nachbedingungen müssen auf das Abstraktionsniveau des
Bytecodes abgebildet werden. Das wird schnell derart komplex, dass
man einen Beweis für die korrekte Abbildung benötigt, bevor man mit
der eigentlichen Verifikation beginnen kann. *g*

- Auch hier hat man das Problem der Schleifeninvarianten. Es gibt
keinen Algorithmus, der für die Verifikation gegen eine Spezifikation
und für die eventuell vorkommenden Schleifen geeignete
Invarianten "berechnen" kann.
Hier ist die Kreativität eines Menschen gefragt und wie Du selber

Post by Ingo Menger
(Praktisch wär das natürlich fast wertlos, da den Beweis, daß eine
Nachbedingung verletzt oder eine Vorbedingung nicht eingehalten ist
kaum einer lesen und verstehen könnte.)

ist die Bytecodeebene nicht das geeignete Abstraktionsniveau zum
Ausleben dieser Kreativität ;-)

Grüße!

[Ingo Menger]

Post by Gerd K.

Post by Ingo Menger
Mal eine theoretische Frage in dem Zusammenhang: Wäre es denn nicht
denkbar, die Prüfungen anhand des generierten Bytecodes zu machen,
denn letzterer hat doch eine feststehende Semantik.

- GOTOs ;-)
Programme mit unbedingten Sprüngen sind so gut wie gar nicht
(gegen eine Spezifikaton) zu verifizieren

Ja, ich vergaß ... die blöden gotos.

Post by Gerd K.
- Auch hier hat man das Problem der Schleifeninvarianten. Es gibt
keinen Algorithmus, der für die Verifikation gegen eine Spezifikation
und für die eventuell vorkommenden Schleifen geeignete
Invarianten "berechnen" kann.

Das hab ich noch nicht ganz verstanden.
Ginge das nicht in zumindest einigen Fällen induktiv?

[Gerd K.]

Post by Ingo Menger

Post by Gerd K.
- Auch hier hat man das Problem der Schleifeninvarianten. Es gibt
keinen Algorithmus, der für die Verifikation gegen eine Spezifikation
und für die eventuell vorkommenden Schleifen geeignete
Invarianten "berechnen" kann.

Das hab ich noch nicht ganz verstanden.
Ginge das nicht in zumindest einigen Fällen induktiv?

Man könnte induktiv beweisen, dass ein Prädikat eine Invariante ist,
aber das Problem ist ja das Finden einer geeigneten Invarianten.
Leider gelingt der Verfikationsbeweis nicht mit jeder...

Bsp:

{Vorbedingung}

S1;

while B do
S_while

{Nachbedingung}

soll als gültig verifiziert werden, heisst: Es soll gezeigt werden,
dass wenn vor Abarbeitung des Programmstücks die Vorbedingung
wahr ist, dann danach auch die Nachbdingung wahr ist.

Mit Hilfe einer beliebigen Invarianten INV bekommt man schnell so was
als gültig heraus:

{INV}
while B do
S_while
{INV and not B}

Das ist etwas, was für die Schleife immer gilt, egal wo
sie verwendet wird. Nun allerdings müssen wir sie in einen
speziellen, durch die Vor- und Nachbedingung und durch den
weiteren Quellcode definierten Kontext
setzen:
{Vorbedingung} ->
{INV'}
S1;
{INV}
while B do
S_while
{INV and not B}
-> {Nachbedingung}

Wobei INV' sich in Abhängikeit der Anweisung S1 direkt aus INV
berechnen läßt (wenn die die Semantik von S1 formal definiert ist).

Nur wenn Vorbedingung => INV' und
INV and not B => Nachbedingung beide wahr sind, ist die Verifikation
gelungen. Das macht das Finden "geeigneter" Invarianten
schwer...

Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hallo Frank!

Post by Frank Buss
Das beweist also zur Compilierzeit, daß der Code die entsprechenden
Nachbedingungen erfüllt. Wie gut es ist, weiß ich allerdings nicht, aber
ich sehe keinen Grund, warum nicht ein Compiler auch automatisch z.B. das
Hoare Kalkül anwenden können sollte, auch für Java.

Das scheitert schon alleine daran, dass es (noch?) keine formale
Semantik von Java gibt, d.h. keine formale Semantikdefinition einer
jeden Java-Anweisung.

ähm Widerspruch.
http://www.ingentaconnect.com/content/maik/pacs/2003/00000029/00000005/00475086
Und ich hatte ein weit älteres Buch auch schon mal in den Händen, wo
es auch um die Semantik der Javaanweisungen ging.

Post by Gerd K.
Das Definieren einer solchen Semantik ist
aktueller Forschungsgegenstand der Informatik.

Dann meinen wir hier verschiedene Dinge. Ich meinte jeden Ausdruck in
Java mittels zum Beispiel Denotationaler Semantik auszudrücken... Es
ging odch um *Formale* Semantik, oder?

Gruss theo

[Jochen Theodorou]

Jochen Theodorou schrieb:
[...]

Und ich hatte ein weit älteres Buch auch schon mal in den Händen, wo es
auch um die Semantik der Javaanweisungen ging.

achja, das war sowas wie
http://www.amazon.de/exec/obidos/ASIN/3540661581/qid%3D1122414693/028-0661668-4036537

Gruss theo

[Stefan Ram]

Post by Jochen Theodorou
Dann meinen wir hier verschiedene Dinge. Ich meinte jeden Ausdruck in
Java mittels zum Beispiel Denotationaler Semantik auszudrücken... Es
ging odch um *Formale* Semantik, oder?

Eine denotationelle Semantik einer Sprache sollte nicht nur
die Bedeutung von Ausdrücken festlegen.

[Jochen Theodorou]

Post by Stefan Ram

Post by Jochen Theodorou
Dann meinen wir hier verschiedene Dinge. Ich meinte jeden Ausdruck in
Java mittels zum Beispiel Denotationaler Semantik auszudrücken... Es
ging odch um *Formale* Semantik, oder?

Eine denotationelle Semantik einer Sprache sollte nicht nur
die Bedeutung von Ausdrücken festlegen.

Mit Ausdrücke meinte ich Expressions und Statements.

Was gibt es denn sonst noch? Meinst du den dispatch bei Methoden?


Gruss theo

[Stefan Ram]

Post by Jochen Theodorou
Mit Ausdrücke meinte ich Expressions und Statements.

"expression" ist ja das englische Wort für einen Ausdruck,
so daß Dein Sprachgebrauch dann vom üblichen abweicht oder
jedenfalls mißverständlich ist.

Eine denotationelle Semantik ordnet jeder Phrase einer Sprache
ein Objekt eines Modells zu.

(Der deutschsprachige Wikipedia-Artikel dazu ist schlecht, der
englischsprachige besser, aber keiner definiert
"denotationelle Semantik" mit derselben Bedeutung wie ich.
Also ist die Bedeutung auch noch etwas umstritten.)

Post by Jochen Theodorou
Was gibt es denn sonst noch?

Wenn eine Semantik von Java nicht erklärt, was beispielsweise
eine Methodendeklaration oder Importdeklaration bedeutet, ist
sie doch keine vollständige Semantik der Sprache.

Im allgemeinen nennt man beliebige solche Teile einer Sprache
"(Nichtterminal-)Symbole", "Phrasen" oder "Klauseln". Sie
bestehen oft aus einem Kern und Satelliten: Der Kern gibt grob
an, was für eine Phrase es ist, die Satelliten dann die
Details. Beispielsweise ist in "2+3" der Kern das "+", und "2"
und "3" sind die Satelliten, in "while(true);" ist
"while(...)" der Kern und "true" und ";" sind die Satelliten.

Java ist ein bewegliches Ziel: In dem Moment, wo irgendjemand
eine formale Semantik von Java veröffentlicht hat, ist diese
auch schon wieder gegenüber der aktuellen Java-Version
veraltet.

Bestimmte native-Methoden müssen vielleicht auch noch als
Teil der formalen Semantik erklärt werden, da sie nicht wie
in Java geschriebene Methoden auf primitive Java-Phrasen
zurückgeführt werden können.

[Jochen Theodorou]

Post by Stefan Ram

Post by Jochen Theodorou
Mit Ausdrücke meinte ich Expressions und Statements.

"expression" ist ja das englische Wort für einen Ausdruck,
so daß Dein Sprachgebrauch dann vom üblichen abweicht oder
jedenfalls mißverständlich ist.
Eine denotationelle Semantik ordnet jeder Phrase einer Sprache
ein Objekt eines Modells zu.
(Der deutschsprachige Wikipedia-Artikel dazu ist schlecht, der
englischsprachige besser, aber keiner definiert
"denotationelle Semantik" mit derselben Bedeutung wie ich.
Also ist die Bedeutung auch noch etwas umstritten.)

also ich dachte immer die Denotationale Semantik ordne jeder "Phrase"
einer Srpache eine Bedeutung in Form einer Funktion zu. Das erlaubt dann
zum Beispiel bei der while-Schleife den Fispunktsatz zu benutzen und
solche Scherze.

Post by Stefan Ram

Post by Jochen Theodorou
Was gibt es denn sonst noch?

Wenn eine Semantik von Java nicht erklärt, was beispielsweise
eine Methodendeklaration oder Importdeklaration bedeutet, ist
sie doch keine vollständige Semantik der Sprache.

das steht ja in der JLS, muss man nur mathematisch formulieren. Bzw.
dann schreibt man für Klassen halt nicht "X" , sonder "resovle(X)" und
definiert X so dass es die Imports nutzt um den Namen aufzulösen. Zum
Beispiel sowas in der art:

Y.X = resolve(X) <==> Es gibt eine Klasse Y.X, Y.X ist der FQN von X, es
gibt eine "import" Anweisung der Form "import Y.*" oder "import Y.X",
oder Y ist java.lang. .X sei hierbei das default package.

Sowas in der Art allerdings unter Nutzung von Mengen und ohne logische
Ausdrücke. Das mit den losigschen Ausdrücken war die andere Semantik...
ähm... axiomatische Semantik war das glaube ich... oder die
operationale... ich konnte mir immer nur die denotationale merken ;)

Post by Stefan Ram
Im allgemeinen nennt man beliebige solche Teile einer Sprache
"(Nichtterminal-)Symbole", "Phrasen" oder "Klauseln". Sie
bestehen oft aus einem Kern und Satelliten: Der Kern gibt grob
an, was für eine Phrase es ist, die Satelliten dann die
Details. Beispielsweise ist in "2+3" der Kern das "+", und "2"
und "3" sind die Satelliten, in "while(true);" ist
"while(...)" der Kern und "true" und ";" sind die Satelliten.

machst du da jetzt nicht einen wilden Mix aus Grammatik und Semantik?

Post by Stefan Ram
Java ist ein bewegliches Ziel: In dem Moment, wo irgendjemand
eine formale Semantik von Java veröffentlicht hat, ist diese
auch schon wieder gegenüber der aktuellen Java-Version
veraltet.

gut, generics und so... aber was bitte ist innerhalb der 1.2, 1.3 und
1.4 Versionen? Ich glaube ich habe da deine Sichtweise noch nicht ganz
kapiert. Klar hat sich da die API geändert, aber die ist normalerweise
nicht Teil der Semantik.

Post by Stefan Ram
Bestimmte native-Methoden müssen vielleicht auch noch als
Teil der formalen Semantik erklärt werden, da sie nicht wie
in Java geschriebene Methoden auf primitive Java-Phrasen
zurückgeführt werden können.

Wie gesagt... die API sit normalerweise nicht Teil der Semantik. Wenn
diese in Java geschrieben ist, dann gibt es ja dazu auch gar keinen
Grund. Wenn der Teil in Java geschrieben werden könnte auch nicht.
native Methoden würde cih nciht als Teil der Semantik der Srpache
definieren, ausser es geht darum wie die Methode aus der Sprache heraus
behandelt wird. Also Typen, Aufruf usw. Was die Funktion macht ist
ausserhalb der Sprache. Ok, so gesehen kann es dann nie eine
Vollständige Semantik geben. Aber das gilt dann für jede Sprache mit
solchen interfaces. Andererseits ist das ein Konstrukt um die Srpache
als solche zu verlassen... warum sollte dafür eine Semantik definiert
werden? Und gerade die Denotationale Semantik will doch ein weitgehend
vom Computermodell unabhängige Semantik schaffen.

Gruss theo

[Stefan Ram]

Post by Jochen Theodorou

Post by Stefan Ram
Eine denotationelle Semantik ordnet jeder Phrase einer Sprache
ein Objekt eines Modells zu.

also ich dachte immer die Denotationale Semantik ordne jeder "Phrase"
einer Srpache eine Bedeutung in Form einer Funktion zu. Das erlaubt dann
zum Beispiel bei der while-Schleife den Fispunktsatz zu benutzen und
solche Scherze.

Das ist mit meiner Definition verträglich, da eine Funktion ja
ein Objekt (eine Entität) eines mathematischen Modells ist.

(In der modernen Standardmathematik sind alle Entitäten, auch
Funktionen, Mengen, so daß man in diesem Fall letztendlich
eine Menge zuordnet.)

Post by Jochen Theodorou
Sowas in der Art allerdings unter Nutzung von Mengen und ohne logische
Ausdrücke. Das mit den losigschen Ausdrücken war die andere Semantik...
ähm... axiomatische Semantik war das glaube ich... oder die
operationale... ich konnte mir immer nur die denotationale merken [...]

Vermutlich die axiomatische.

Post by Jochen Theodorou

Post by Stefan Ram
Im allgemeinen nennt man beliebige solche Teile einer Sprache
"(Nichtterminal-)Symbole", "Phrasen" oder "Klauseln". Sie
bestehen oft aus einem Kern und Satelliten: Der Kern gibt grob
an, was für eine Phrase es ist, die Satelliten dann die
Details. Beispielsweise ist in "2+3" der Kern das "+", und "2"
und "3" sind die Satelliten, in "while(true);" ist
"while(...)" der Kern und "true" und ";" sind die Satelliten.

machst du da jetzt nicht einen wilden Mix aus Grammatik und Semantik?

Na gut, dann streiche ich den Teil mit Kernen und Satelliten
wieder.

Aber im allgemeinen bezieht sich die Semantik auf die Syntax,
da sie die Bedeutung der syntaktisch möglichen Konstrukte
angibt.

Post by Jochen Theodorou

Post by Stefan Ram
Java ist ein bewegliches Ziel: In dem Moment, wo irgendjemand
eine formale Semantik von Java veröffentlicht hat, ist diese
auch schon wieder gegenüber der aktuellen Java-Version
veraltet.

gut, generics und so... aber was bitte ist innerhalb der 1.2, 1.3 und
1.4 Versionen? Ich glaube ich habe da deine Sichtweise noch nicht ganz
kapiert. Klar hat sich da die API geändert, aber die ist normalerweise
nicht Teil der Semantik.

Ich hatte nicht daran gedacht, daß die Sprache wirklich eine
Zeit lang konstant war.

Post by Jochen Theodorou
Was die Funktion macht ist ausserhalb der Sprache.

Das kommt darauf an, in welchem Umfang man Java formalisieren
will. java.lang.String-Methoden stehen ja teilweise auch in
der JLS.

Wenn man eine formale Semantik von Java praktisch anwenden
will, dann sollte diese realistische Java-Programme
beschreiben können, und die verwenden die Standard-API.

Ist die Standard-API selber mit Java definiert, so kann
man dies an Hand dieser Definitionen automatisch auf die
bereits vorhandene Semantik zurückführen. Dies scheitert
aber bei nativen Methoden.

[Jochen Theodorou]

[...]

Post by Stefan Ram

Post by Jochen Theodorou
machst du da jetzt nicht einen wilden Mix aus Grammatik und Semantik?

Na gut, dann streiche ich den Teil mit Kernen und Satelliten
wieder.
Aber im allgemeinen bezieht sich die Semantik auf die Syntax,
da sie die Bedeutung der syntaktisch möglichen Konstrukte
angibt.

Das ist aber nicht unbedingt ein Grund eine Grammatik in die Semantik zu
mischen. Die Grammatik definiert die Syntax, die Semantik gibt einem
Programm dessen Bedeutung. Bei der Grammatik steght stehen die Regeln
zur erzeugung der Programme im Vodergrund und bei der Semantik die
Regeln zur Besetzung der syntaktischen Gerippe mit Bedeutung. Klar haben
die was miteinander zu tun... halt wie Socken und Schuhe ;) Und zum
putzen der Schuhe benutze ich normalerweise einen Lappen oder eine
Bürste... je nachdem. Ich kann mir jetzt einen Socken als Lappen
definieren, dann passt das schon, aber das ist eher unerheblich.

Post by Stefan Ram

Post by Jochen Theodorou

Post by Stefan Ram
Java ist ein bewegliches Ziel: In dem Moment, wo irgendjemand
eine formale Semantik von Java veröffentlicht hat, ist diese
auch schon wieder gegenüber der aktuellen Java-Version
veraltet.

gut, generics und so... aber was bitte ist innerhalb der 1.2, 1.3 und
1.4 Versionen? Ich glaube ich habe da deine Sichtweise noch nicht ganz
kapiert. Klar hat sich da die API geändert, aber die ist normalerweise
nicht Teil der Semantik.

Ich hatte nicht daran gedacht, daß die Sprache wirklich eine
Zeit lang konstant war.

In 1.1 war sie das glaube ich länger. 1.5 und 1.6 sind ja auch nciht
wirklich mit Sprachänderungen gepflastert. Wirklich neues ist ja für die
Semantik nur in 1.5 mit den Generics hinzu gekommen. Wenn sie das mit
den Closures umsetzen in java7, dann wird auch wieder was semantisch
neues, weil einerseits die generics geändert werden und andererseits
teilweise typen automatisch ermittelt werden. Aber da muss man noch
abwarten was davon am Ende überhaupt übrig bleibt.

Post by Stefan Ram

Post by Jochen Theodorou
Was die Funktion macht ist ausserhalb der Sprache.

Das kommt darauf an, in welchem Umfang man Java formalisieren
will. java.lang.String-Methoden stehen ja teilweise auch in
der JLS.

die JLs ist keine Denotationale Semantik ;) Das steht da drin, weil es
für den Anwender wichtig ist. die Formale Sicht interessiert sich für
den Anwender der zu untersuchenden Sprache herzlich wenig.

Post by Stefan Ram
Wenn man eine formale Semantik von Java praktisch anwenden
will, dann sollte diese realistische Java-Programme
beschreiben können, und die verwenden die Standard-API.
Ist die Standard-API selber mit Java definiert, so kann
man dies an Hand dieser Definitionen automatisch auf die
bereits vorhandene Semantik zurückführen. Dies scheitert
aber bei nativen Methoden.

und ist das für die nativen Methoden so schlimm?

Gruss theo

[Stefan Ram]

Post by Stefan Ram
Das kommt darauf an, in welchem Umfang man Java formalisieren
will. java.lang.String-Methoden stehen ja teilweise auch in
der JLS.

die JLs ist keine Denotationale Semantik [...] Das steht da
drin, weil es für den Anwender wichtig ist.

Die JLS definiert die Sprache Java. Wenn man diese formal
beschreiben will, muß man also das formalisieren, was in der
JLS steht. Insbesondere sind die java.lang.String-Methoden
damit ein Teil der Sprache Java.

Post by Stefan Ram
Ist die Standard-API selber mit Java definiert, so kann
man dies an Hand dieser Definitionen automatisch auf die
bereits vorhandene Semantik zurückführen. Dies scheitert
aber bei nativen Methoden.

und ist das für die nativen Methoden so schlimm?

Es erhöht den Aufwand für den Autor der formalen
Spezifikation.

[Ingo R. Homann]

Hi,

Post by Stefan Ram
"expression" ist ja das englische Wort für einen Ausdruck,
so daß Dein Sprachgebrauch dann vom üblichen abweicht oder
jedenfalls mißverständlich ist.

Haha! Das kommt ja genau vom Richtigen! ;-)

Post by Stefan Ram
(...keiner definiert
"denotationelle Semantik" mit derselben Bedeutung wie ich.
Also ist die Bedeutung auch noch etwas umstritten.)

Hohoho, es wird immer besser...

ROTFLOL

SCNR,
Ingo

[Stefan Ram]

(...keiner definiert "denotationelle Semantik" mit derselben
Bedeutung wie ich. Also ist die Bedeutung auch noch etwas
umstritten.)

»Konstruktion der Semantik mittels mathematischer Räume aus
der Bereichstheorie; die Semantik eines Programms ist eine
Funktion.«

http://de.wikipedia.org/wiki/Formale_Semantik

»each phrase in the language is translated into a
denotation, i.e. a phrase in some other language.«

http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages

Du solltest erkennen können, daß diese beiden Beschreibungen
der denotationellen Semantik sich stark unterscheiden.

Die erste erscheint mir als zu speziell und die zweite
verwendet Zielphrasen einer Zielsprache, was mir als unüblich
erscheint.

Nach dem Verfassen meines vorherigen Beitrags entdeckte ich
dann in der Wikipädie auch noch:

»constructing mathematical objects (called denotations or
meanings) which express the semantics«

http://en.wikipedia.org/wiki/Denotational_semantics

Was meiner eigenen Definition am nächsten kommt.

[Ingo R. Homann]

Hi,

(...keiner definiert "denotationelle Semantik" mit derselben
Bedeutung wie ich. Also ist die Bedeutung auch noch etwas
umstritten.)

[...]

Es mag ja sein, dass Du in der Sache Recht hast (ich habe das nicht
überprüft) - nur... Du hast es vielleicht etwas ungünstig formuliert...
nix für ungut.

Ciao,
Ingo

[Gerd K.]

Hallo Jochen!

Post by Jochen Theodorou
Dann meinen wir hier verschiedene Dinge. Ich meinte jeden Ausdruck in
Java mittels zum Beispiel Denotationaler Semantik auszudrücken... Es
ging odch um *Formale* Semantik, oder?

Da es in der Diskussion um Verifikation geht, habe ich formale
Semantik implizit mit axiomatischer Semantik gleichgesetzt, denn nur
diese
spielt bei der Verifikation gegen die Spezifikation eine Rolle.
Ersetze in meinen Aussagen einfach formale Semantik durch
axiomatische Semantik.

Eine prima Einleitung zu der ganzen Thematik ist z.B. hier zu
finden:
http://www.dbis.informatik.uni-frankfurt.de/TEACHING/INFO2/2003_SS/pi2_kap3.pdf

Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hallo Jochen!

Post by Jochen Theodorou
Dann meinen wir hier verschiedene Dinge. Ich meinte jeden Ausdruck in
Java mittels zum Beispiel Denotationaler Semantik auszudrücken... Es
ging odch um *Formale* Semantik, oder?

Da es in der Diskussion um Verifikation geht, habe ich formale
Semantik implizit mit axiomatischer Semantik gleichgesetzt, denn nur
diese
spielt bei der Verifikation gegen die Spezifikation eine Rolle.
Ersetze in meinen Aussagen einfach formale Semantik durch
axiomatische Semantik.

Und ich dachte immer axiomatische Semantik sei ein Teil der formalen.
Mehr, noch, es gäbe einen BEweiss der die axiomatische and denotationale
Semantik gleichsetzt von ihrer Mächtigkeit her. Der Grund warum das
automatische Beweisen eher der axiomatischen Semantik überlassen ist
dürfte darin liegen, dass sich automatische Beweissysteme besser mit
Logischen Formeln erstellen lassen - IMHO ;) Mit Funktionen geht das
sicher auch, aber dann muss man Symbolbasierende berechnungen machen und
irgendwie kenne ich fast nur kommerzielles in dem Bereich.

Post by Gerd K.
Eine prima Einleitung zu der ganzen Thematik ist z.B. hier zu
http://www.dbis.informatik.uni-frankfurt.de/TEACHING/INFO2/2003_SS/pi2_kap3.pdf

Das ist höchstens ein Streifzug, keine Einführung

Post by Gerd K.
Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Das mit dem niemals würde ich so nicht stehen lassen... Die Ewigkeit ist
eine solch lange Zeit.

Gruss theo

[Gerd K.]

Post by Jochen Theodorou

Post by Gerd K.
Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Das mit dem niemals würde ich so nicht stehen lassen... Die Ewigkeit ist
eine solch lange Zeit.

Aber hier kann das 'niemals' mit Sicherheit stehen bleiben. ;-)
Das hat die theoretische Informatik i.A. bewiesen...

Grüße!

[Ingo Menger]

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Das mit dem niemals würde ich so nicht stehen lassen... Die Ewigkeit ist
eine solch lange Zeit.

Aber hier kann das 'niemals' mit Sicherheit stehen bleiben. ;-)
Das hat die theoretische Informatik i.A. bewiesen...

Hat sie nicht vielmehr das Gegenteil bewiesen? Stichwort
http://en.wikipedia.org/wiki/Curry-Howard_isomorphism

Eines Tages werden wir hinschreiben, was wir beweisen wollen
(Spezifikation), dann werden wir den Beweis (das Programm) hinschreiben
und einen automatischen Beweisverifizierer nachprüfen lassen, daß wir
keinen Fehler gemacht haben.

[Gerd K.]

Post by Ingo Menger
Hat sie nicht vielmehr das Gegenteil bewiesen?

Nein. ;-)
Eine Beweiskizze:

Angenommen, es gebe ein Funktion stoppt, die sagt, ob ein
beliebiges Programm bei einer beliebigen Eingabe terminiert,
also
stoppt(x,y)=true, falls das x.Programm bei
Eingabe von y terminiert.
(Da es nur abzählbar unendliche viele Programme gibt,
kann man sich diese geordnet vorstellen...)

Man betrachtet den Algorithmus A:
readln(zahl);
if stoppt(zahl,zahl) then
while true do

Da es nur abzählbar viele Programme gibt, existiert
eine natürliche Zahl r mit r.Programm=A

Jetzt gibt man dieses r in A ein:

Wenn in A stoppt(r,r) true dann Endlosschleife
=>Widerspruch, denn das r.te Programm terminiert
offensichtlich nicht

Wenn in A stoppt(r,r) false dann ist der Algorithmus sofort
beendet => Widerspruch, r muss bei Eingabe von r
endlos laufen.

Solch eine Funktion stoppt kann also nicht existieren.

Wäre die Verifikation gegen eine Spezifikation
entscheidbar, dann könnte man einfach

stoppt(x,y) := Ist x.tes Programm bzgl. der
Spezifikation: {Eingabe y} S {true}
total korrekt?

definieren, und hätte eine Funktion stoppt, die
sagt, ob das x. Programm bei Eingabe von y hält.

Aber da eine solche Funktion nicht existieren kann...

Post by Ingo Menger
Stichwort
http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
Eines Tages werden wir hinschreiben, was wir beweisen wollen
(Spezifikation), dann werden wir den Beweis (das Programm) hinschreiben
und einen automatischen Beweisverifizierer nachprüfen lassen, daß wir
keinen Fehler gemacht haben.

Das ist aber eine ganz andere Qualität als das Berechnen des Beweises
selber. Es geht doch gerade um das Finden eines solchen, nicht
um die Verifizierung, dass es auch ein Beweis ist.

Grüße!

[Jochen Theodorou]

Gerd K. schrieb:
[Halteproblem]

Das mag ja alles stimmen.. aber die Realität sieht anders aus. Dort
bekommt ein Programm nicht eine beliebige Zahl, sondern eine Zahl aus
einer definierten endlichen Wertemenge (zumindest durch den verfügbaren
Speicherplatz begrenzt). Und natürlich ist es einleuchtend, das wenn ich
ein Programm ausführe und dies in eine Endlosschleife gerät, dieses dann
nicht hält. Wenn ich aber die Struktur des Programmes untersuche wird
die Schleife eventuell erkannt. Unter bestimmten prämissen geht das auch
wenn man das Programm leicht verändert ausführt. Wenn ich zum Beispiel
den relevanten Speicherzustand mit hineinnehme, dann kann ich für jede
Schleifenausführung diesen Protkollieren und im Falle einer Wiederholung
abbrechen. Das funktioniert nicht nur für Schleifen, auch für verkettete
Funktionen. Da nur endlich viele Eingaben untersucht werden erhält man
in endlicher Zeit eine Lösung. Die mag zwar weiterhin länger sein als
das Universum lebt und mehr Speicher kosten als es Atome im Univerum
gibt, aber es wäre eine Lösung. Was eine abzählbar unendliche Menge von
Programmen und Eingaben angeht stimme ich dir aber durchaus zu.

So sage ich dass die Menge der JVM Bytecodeprogramme endlich ist, wenn
man eine Maximalgrösse für die Klasse vorraussetzt. Die Größe mag
beliebig gross sein, aber endlich. Dann funktioniert die Verkettung der
stoppt-Funktion mit sich selbst schon nicht mehr beliebig oft, weil das
Programm irgendwann zu gross wird.

Gruss theo

[Gerd K.]

Post by Jochen Theodorou
Wenn ich zum Beispiel
den relevanten Speicherzustand mit hineinnehme, dann kann ich für jede
Schleifenausführung diesen Protkollieren und im Falle einer Wiederholung
abbrechen. Das funktioniert nicht nur für Schleifen, auch für verkettete
Funktionen. Da nur endlich viele Eingaben untersucht werden erhält man
in endlicher Zeit eine Lösung.

Diese Argumentation wirft ein Problem auf:

Wenn Du sicherstellen willst, dass das Vorliegen eines Zyklus im
Zustandsgraphen des Systems notwendig für das Vorliegen einer
Endlosschleife ist, musst Du schon einige Klimmzüge veranstalten,
um einen solchen Graphen überhaupt definieren zu können ;-)
Dass das Vorliegen eines Zyklus hinreichend für die Nichtterminierung
ist, geschenkt... ;-) Aber die Nichtterminierung heisst nicht
automatisch,
dass es einen Zyklus geben muss.
Die Generierung eines solchen besonderen Zustandsgraphen muss automa-
tisierbar sein, sonst bricht die Argumentation zusammen.
Mehr als Semientscheidbarkeit ist aber auch dann nicht zu bekommen...

Man kann über die Theorie (der Informatik) denken was man will, aber
sie ist in meinen Augen auf jeden Fall etwas, was jeder, der ernsthaft
Programme schreiben will, mal gesehen haben sollte! Das hilft
immens, über den Tellerrand eines "normalen" Programmierers hinauszu-
schauen und lehrt vielleicht auch etwas "Achtung" vor der Komplexität
des Erzeugens hochwertiger, "korrekter" Software und erklärt u.a.
warum ein Informatikstudium Diplom oder Master vier Jahre dauert.
Und das ist nach Aussage der Experten der erfoderliche Abschluss, um
qualitativ hochwertige Software entwickeln zu können:
drops.dagstuhl.de/opus/volltexte/2006/585/pdf/05402.Manifest_SE_Dagstuhl_IS.585.pdf
Seite 13, dritter Abschnitt

Grüße!

[Jochen Theodorou]

Post by Gerd K.

Post by Jochen Theodorou
Wenn ich zum Beispiel
den relevanten Speicherzustand mit hineinnehme, dann kann ich für jede
Schleifenausführung diesen Protkollieren und im Falle einer Wiederholung
abbrechen. Das funktioniert nicht nur für Schleifen, auch für verkettete
Funktionen. Da nur endlich viele Eingaben untersucht werden erhält man
in endlicher Zeit eine Lösung.

Wenn Du sicherstellen willst, dass das Vorliegen eines Zyklus im
Zustandsgraphen des Systems notwendig für das Vorliegen einer
Endlosschleife ist, musst Du schon einige Klimmzüge veranstalten,
um einen solchen Graphen überhaupt definieren zu können ;-)

Klimmzüge heisst nicht das es unmöglich ist.

Post by Gerd K.
Dass das Vorliegen eines Zyklus hinreichend für die Nichtterminierung
ist, geschenkt... ;-) Aber die Nichtterminierung heisst nicht
automatisch, dass es einen Zyklus geben muss.

Warum terminidert ein Programm sonst nicht? Wohlgemerkt, ich rede davon
dass das Programm nur endlich viele Zustände überhaupt haben kann. Und
das versuche ich durch meine Randbedingungen mit dem endlichen Speicher
(sowhol für das Programm als auch für die Ausführung des Programms) und
der endlichen Anzahl verfügbarer Werte zu untermauern.

Post by Gerd K.
Die Generierung eines solchen besonderen Zustandsgraphen muss automa-
tisierbar sein, sonst bricht die Argumentation zusammen.

oh, automatisierbar ist es ganz bestimmt. Ob es was nutzt ist eine
andere Frage

Post by Gerd K.
Mehr als Semientscheidbarkeit ist aber auch dann nicht zu bekommen...

weil?

Post by Gerd K.
Man kann über die Theorie (der Informatik) denken was man will, aber
sie ist in meinen Augen auf jeden Fall etwas, was jeder, der ernsthaft
Programme schreiben will, mal gesehen haben sollte! Das hilft
immens, über den Tellerrand eines "normalen" Programmierers hinauszu-
schauen und lehrt vielleicht auch etwas "Achtung" vor der Komplexität
des Erzeugens hochwertiger, "korrekter" Software und erklärt u.a.
warum ein Informatikstudium Diplom oder Master vier Jahre dauert.
Und das ist nach Aussage der Experten der erfoderliche Abschluss, um
drops.dagstuhl.de/opus/volltexte/2006/585/pdf/05402.Manifest_SE_Dagstuhl_IS.585.pdf
Seite 13, dritter Abschnitt

und was genau willst du mir damit sagen? Ich hatte theoretische
Informatik. Zusammengerechnet kommt dabei bestimmt mehr al ein Semester
pure theoretische Informatik heraus.

aber gerade deswegen find ich, man muss die Aussagen der theoretischen
Informatik relativieren. Und nur weil man Klimzüge machen muss heisst
das noch lange nicht, dass es nciht geht. Das ehisst nur dass es an
Ausdrucksfähigkeit mangelt.

Aber wie gesagt, aus der Erkenntnis dass man für endliche mögliche
Zustände das Halteproblem eventuell lösen kann erwächst noch lange kein
praktischer Nutzen

Gruss theo

[Wanja Gayk]

Post by Jochen Theodorou
Warum terminidert ein Programm sonst nicht?

Der simpelste Fall ist, dass ein Programm seine eigene Korrektheit
bewerten soll.
Sprich: damit ein Programm entscheiden kann, ob es selbst terminiert,
muss es entscheiden, ob es selbst terminiert, was es nur kann, wenn es
selbst terminiert.. du erkennst die Endlosrekursion?

Etwas mathematischer ausgedrückt wäre es so:
gegeben sei eine Funktion f(g(x)) für die gilt:
f(g(x)) = 1, wenn g(x) = 0
f(g(x)) = 0, wenn g(x) = 1

Welches Ergebnis hat dann der Fall f = g, also f(f(x))?
Richtig: das ist unentscheidbar.
Seit kurt Gödel wissen wir nun, dass alles, was berechenbnar ist auch
RAM-Berechenbar ist, bzw. mit einer Turingmaschine. Ergo lösst sich
jedes Programm als mathamatische Funktion ausdrücken und umgekehrt. Weil
es unentscheidbare Funktionen gibt, gibt es demzufolge quch
unentscheidbare Programme. Das programm, welches für alle Programme
feststellen soll, ob es terminiert gehört dazu, denn es leidet an dem
o.G. Diagonalisierungsproblem - und einigen andren.

Diese diagonalisierungsfunktion kannman auch nicht einfach abfangen,
weil man dazu erstmal die Äquivalenz von 2 Funktionen für die gegebene
Eingabe beweisen müsste. Dummerweise kannst da aber nicht jede mögliche
Eingabe berechnen, denn davon gibt es möglicherweie unendlich viele.
Böse Falle!

Ein weiteres, noch einfacheres Beispiel, warum es nicht funktioniert:
Frage: terminiert folgende Methode?

public void willIStop(InputStream stream){
int input;
while(input = stream.read() != -1){
System.out.print(input);
}
}

Antwort: das ist nicht entscheidbar.
Du kannst nämlich nicht wissen, ob die Datenquelle jemals eine -1 senden
wird - die Datenquelle muss ja kein Programm sein, sondern kann auch ein
Messgerät sein oder wasauchimmer. Wenn das für fünf Milliarden
Iterationen nicht der Fall war, könnte es bei der fünfmiliardenundersten
Iteration der Fall sein.. oder auch nicht - wohger will man das wissen?

Gruß,
-Wanja-

[Jochen Theodorou]

Post by Wanja Gayk

Post by Jochen Theodorou
Warum terminidert ein Programm sonst nicht?

Der simpelste Fall ist, dass ein Programm seine eigene Korrektheit
bewerten soll.
Sprich: damit ein Programm entscheiden kann, ob es selbst terminiert,
muss es entscheiden, ob es selbst terminiert, was es nur kann, wenn es
selbst terminiert.. du erkennst die Endlosrekursion?

Das sit auch nur eine Schleife. Ob du das jetzt Rekursiv machst, oder
nicht ist egal.

Post by Wanja Gayk
f(g(x)) = 1, wenn g(x) = 0
f(g(x)) = 0, wenn g(x) = 1
Welches Ergebnis hat dann der Fall f = g, also f(f(x))?
Richtig: das ist unentscheidbar.

Vielleicht für alle x aus einer unendlichen Menge, aber bei einer
endlichen Menge ist es das sehr wohl

Post by Wanja Gayk
Seit kurt Gödel wissen wir nun, dass alles, was berechenbnar ist auch
RAM-Berechenbar ist, bzw. mit einer Turingmaschine. Ergo lösst sich
jedes Programm als mathamatische Funktion ausdrücken und umgekehrt. Weil
es unentscheidbare Funktionen gibt, gibt es demzufolge quch
unentscheidbare Programme. Das programm, welches für alle Programme
feststellen soll, ob es terminiert gehört dazu, denn es leidet an dem
o.G. Diagonalisierungsproblem - und einigen andren.

eben nicht "für alle Programme"!

Post by Wanja Gayk
Diese diagonalisierungsfunktion kannman auch nicht einfach abfangen,
weil man dazu erstmal die Äquivalenz von 2 Funktionen für die gegebene
Eingabe beweisen müsste. Dummerweise kannst da aber nicht jede mögliche
Eingabe berechnen, denn davon gibt es möglicherweie unendlich viele.
Böse Falle!

Und ich sprach von endlicher Eingabe.

Post by Wanja Gayk
Frage: terminiert folgende Methode?
public void willIStop(InputStream stream){
int input;
while(input = stream.read() != -1){
System.out.print(input);
}
}
Antwort: das ist nicht entscheidbar.
Du kannst nämlich nicht wissen, ob die Datenquelle jemals eine -1 senden
wird - die Datenquelle muss ja kein Programm sein, sondern kann auch ein
Messgerät sein oder wasauchimmer.

Du willst auf Nichtdeterminismus hinaus denke ich. Bedenke aber dass
sich ejdes Nichtdeterministische endliche System durch ein
Deterministisches ersetzen lässt. siehe dazu auch die Transformation von
Nichtdeterministischen Automaten in deterministische.

Post by Wanja Gayk
Wenn das für fünf Milliarden
Iterationen nicht der Fall war, könnte es bei der fünfmiliardenundersten
Iteration der Fall sein.. oder auch nicht - wohger will man das wissen?

bei welcher das genau ist ist irrelevant. Wichtig ist nur dass es nur
endlich viele Möglichkeiten gibt.

Gruss theo

[Wanja Gayk]

Post by Jochen Theodorou

Post by Wanja Gayk
Diese diagonalisierungsfunktion kannman auch nicht einfach abfangen,
weil man dazu erstmal die Äquivalenz von 2 Funktionen für die gegebene
Eingabe beweisen müsste. Dummerweise kannst da aber nicht jede mögliche
Eingabe berechnen, denn davon gibt es möglicherweie unendlich viele.
Böse Falle!

Und ich sprach von endlicher Eingabe.

Ein Block von 1 GB Daten ist auch eine endliche Eingabe, aber probier
mal alle Permutationen möglicher 1GB großer Eingaben durch, um darauf zu
kommen, ob ein Algorithmus der eine bestimmte Escape-Sequenz erwartet
bei diesen Daten terminiert (ob mit einer Exception oder nicht sei
dahingestellt).

Post by Jochen Theodorou

Post by Wanja Gayk
Frage: terminiert folgende Methode?
public void willIStop(InputStream stream){
int input;
while(input = stream.read() != -1){
System.out.print(input);
}
}
Antwort: das ist nicht entscheidbar.
Du kannst nämlich nicht wissen, ob die Datenquelle jemals eine -1 senden
wird - die Datenquelle muss ja kein Programm sein, sondern kann auch ein
Messgerät sein oder wasauchimmer.

Du willst auf Nichtdeterminismus hinaus denke ich.

Nein, hier irrst du.
Schau nochmal hin:

Es geht darum, ob die Datenquelle jemals ein -1 bereit stellen wird.
Die Datenquelle kann absolut deterministisch sein, das ist sie auch,
wenn sie aus einer Endlosschleife besteht, die nur das Byte 2 sendet.
Allerdings kannst du ohne Kenntnis der Datenquelle nicht auf die
Korrektheit dieser Methode schließen.
Dummerweise ist diese Methode nämlich unabhängig von einer bestemmten
Datenquelle, diese Quelle lässt sich jederzeit austauschen.

Mit anderen Worten ist diese Methode in einem Kontext terminierend, in
einem anderen nicht. Java ist eine dynamische Sprache, du kannst den
Kontext beliebig während der Laufzeit ändern.

Genauergesagt ist diese Methode so lange Schrödingers Katze, bis zu
definitiv sagen kannst, welche Quelle dran hängt und bis du definitiv
sagen kannst, dass diese Quelle das gewünschte liefern wird und bis du
definitiv sagen kannst, dass diese Quelle nicht mehr ausgetauscht wird.
Letzteres ist spätestens dann unmöglich, wenn der InputStream über ein
Netzwerk bedient wird in dem du die Implementation der Quelle gar nicht
kennen kannst. Selbst wenn du das aber noch beweisen könntest, ist der
Aufwand schätzungsweise alles andere als nur polynomiell.
Kurzum: Alleine die Korrektheit dieser kleinen Methode ist nicht
entscheidbar.

Gruß,
-Wanja-

[Jochen Theodorou]

Post by Wanja Gayk

Post by Jochen Theodorou

Post by Wanja Gayk
Diese diagonalisierungsfunktion kannman auch nicht einfach abfangen,
weil man dazu erstmal die Äquivalenz von 2 Funktionen für die gegebene
Eingabe beweisen müsste. Dummerweise kannst da aber nicht jede mögliche
Eingabe berechnen, denn davon gibt es möglicherweie unendlich viele.
Böse Falle!

Und ich sprach von endlicher Eingabe.

Ein Block von 1 GB Daten ist auch eine endliche Eingabe, aber probier
mal alle Permutationen möglicher 1GB großer Eingaben durch, um darauf zu
kommen, ob ein Algorithmus der eine bestimmte Escape-Sequenz erwartet
bei diesen Daten terminiert (ob mit einer Exception oder nicht sei
dahingestellt).

ich glaube ähnliches habe ich bereits 3x in diesem Thread gesagt oder?
Sicher nciht über Permutationen oder 1GB, aber darüber das aus dem
Wissen dass ich das entscheiden kann noch lange etwas praxisrelevantes
entsteht.

Post by Wanja Gayk

Post by Jochen Theodorou

Post by Wanja Gayk
Frage: terminiert folgende Methode?
public void willIStop(InputStream stream){
int input;
while(input = stream.read() != -1){
System.out.print(input);
}
}
Antwort: das ist nicht entscheidbar.
Du kannst nämlich nicht wissen, ob die Datenquelle jemals eine -1 senden
wird - die Datenquelle muss ja kein Programm sein, sondern kann auch ein
Messgerät sein oder wasauchimmer.

Du willst auf Nichtdeterminismus hinaus denke ich.

Nein, hier irrst du.
Es geht darum, ob die Datenquelle jemals ein -1 bereit stellen wird.
Die Datenquelle kann absolut deterministisch sein, das ist sie auch,
wenn sie aus einer Endlosschleife besteht, die nur das Byte 2 sendet.

Ok, dann etwas formaler...

Sei c eine Anweiseung, sei v der Zustand des Systems
Es gilt v --c--> v', also c überführt ein bestimmtes v in v'. Ein
Programm bestehe nun aus einer Verkettung von cs, also "c1; c2; c3" usw.
Jedes c1 überführt v in v1, c2 überführt v1 in v2 usw. Sei cr der Rest
des noch auszuführenden Programmes. Sammele ich nun all diese (vi,cr1),
dann kann ich eine Endlosschleife dann feststellen, wenn sich ein
(vj,cr2) findet mit vj=v1 und cr1 = cr2. Das kann ich annehmen aufgrund
der Transitivität. Allein der Nichtdeterminismus kann hier einen Strich
durch die Rechnung machen.

Post by Wanja Gayk
Allerdings kannst du ohne Kenntnis der Datenquelle nicht auf die
Korrektheit dieser Methode schließen.

Dann hast du eine externe Quelle, dein Zustand v ist unvollständig, ich
habe ein vollständig System vorrausgesetzt. Das System lässt sich
vervollständigen indem man den worstcase annimt, also alle möglichen
Werte. Da das endlich viele sind ist das theoretisch kein Problem.
Praktisch natürlich sehr wohl.

Post by Wanja Gayk
Dummerweise ist diese Methode nämlich unabhängig von einer bestemmten
Datenquelle, diese Quelle lässt sich jederzeit austauschen.

sie ist nicht unabhängig! Eine abstrahierung einer Abhängigkeit macht
noch lange keine Unabhängigkeit daraus. Sie ist unabhängig von einer
bestimmten Implementierung wäre korrekter.

Post by Wanja Gayk
Mit anderen Worten ist diese Methode in einem Kontext terminierend, in
einem anderen nicht. Java ist eine dynamische Sprache, du kannst den
Kontext beliebig während der Laufzeit ändern.

Jetzt kommst du noch mit dynamisch... Ich glaube damit verlässt du die
Begrifflichkeiten, die wir gemeinsam haben könnten. Gibt es den
Programmiersprachen in denen ich sowas nicht machen kann?

[...]

Post by Wanja Gayk
Kurzum: Alleine die Korrektheit dieser kleinen Methode ist nicht
entscheidbar.

siehste.. du redest von Korrektheit, ich vom Terminieren.

Gruss theo

[Ralf Ullrich]

Hi Jochen, Gerd, Wanja, etc.

Ich habe eure Diskussion nicht im Detail verfolgt, und zwar weil es müssig
ist für Java darüber zu disktuieren ob man die Korrektheit/Terminierung
eines Programms beweisen kann.

Anbei ein Beispiel für ein Java Programm, dass auf den meisten
Einprozessor-Rechnern, die Java Programme ausführen können beinahe sofort
terminiert, allerdings mit einem mehr oder weniger zufälligen Ergebnis.
(Und das liegt eigentlich nicht daran, dass java.util.Random verwendet
wird.)

Auf einem Mehrprozessorsystem hingegen wird dasselbe Program womöglich
ewig laufen.


Angenommen es gäbe eine Methode anhand eines Programmtextes zu beweisen,
dass ein Programm terminiert, dann müsste diese Methode für das
Beispielprogramm zwei gegensätzliche Ergebnisse liefern, und das bei
gleicher "Eingabe".

Und warum gibt das Programm eigentlich nicht jedesmal die gleiche Zahl
aus? Ich meine das Programm verlangt keinerlei Eingaben, verwendet keine
APIs die veränderliche Werte zurückgeben (wie System.currentTimeMillis()).
Warum?

Mit der gleichen Antwort, die ihr hoffentlich alle auf dieses Warum
findet, kann man auch jeden Versuch die Korrektheit eines nicht trivialen
Java-Programms zu beweisen, von vornherein in den Wind schlagen.

cu

package de.jnana.dclj;

import java.util.Random;
import java.util.concurrent.atomic.AtomicBoolean;
import java.util.concurrent.atomic.AtomicInteger;

public class Deterministic {

public static void main(String[] args) throws Exception {
final AtomicBoolean continu = new AtomicBoolean(true);
final AtomicInteger i = new AtomicInteger();
final AtomicInteger r = new AtomicInteger();
Thread wobbler = new Thread() {
@Override
public void run() {
Random rnd = new Random(0);
while (continu.get()) {
i.set(rnd.nextInt());
}
}
};
Thread sniffer = new Thread() {
@Override
public void run() {
boolean oddeven = false;
int count = 0;
while (continu.get()) {
if (oddeven) {
while (1 == (i.get() & 1)) {
count++;
}
} else {
while (0 == (i.get() & 1)) {
count++;
}
}
if (count > 1000) {
r.set(count);
continu.set(false);
break;
}
oddeven = !oddeven;
count = 0;
}
}
};
wobbler.start();
sniffer.start();
wobbler.join();
System.out.println(r.get());
}

}

[Stefan Ram]

Post by Ralf Ullrich
Angenommen es gäbe eine Methode anhand eines Programmtextes zu
beweisen, dass ein Programm terminiert, dann müsste diese
Methode für das Beispielprogramm zwei gegensätzliche Ergebnisse
liefern, und das bei gleicher "Eingabe".

Einige bekannte Aussagen zum Halteproblem finden sich
beispielsweise in:

http://de.wikipedia.org/wiki/Halteproblem

Du hast also noch einmal ein Beispiel dazu geliefert, das
wohl mit dem Bekannten (aus obigem Wikipädie-Artikel)
verträglich ist.

Post by Ralf Ullrich
Mit der gleichen Antwort, die ihr hoffentlich alle auf dieses
Warum findet, kann man auch jeden Versuch die Korrektheit eines
nicht trivialen Java-Programms zu beweisen, von vornherein in
den Wind schlagen.

Man kann sich ja auf eine Teilmenge von Java beschränken,
bei der so etwas möglich ist.

Oder - wenn, man wie bei Deinem Programm globale Aussagen
nicht mehr machen kann - man kann wenigstens Aussagen über
Programmteile beweisen.

Formale Methoden werden bei Reinraumentwicklungen verwendet:

»The approach combines mathematical-based methods of
software specification, design and correctness
verification with statistical, usage-based testing to
certify software fitness for use.«

http://www.rspa.com/reflib/Cleanroom.html

"There is now compelling evidence that development methods
that focus on bug prevention rather than bug detection can
both raise quality and save time and money."

http://www.stsc.hill.af.mil/crosstalk/2002/08/mosemann.html

Weitere Quellen:

http://www.sei.cmu.edu/pub/documents/96.reports/pdf/tr022.96.pdf
http://web.archive.org/web/20030724121057/http://sern.ucalgary.ca/~hongm/seng/621/SENG621_ESSAY.html
http://www.criticaljunction.com/werbicki/SENG623/Group/SENG623W03_Cleanroom.pdf

[Ralf Ullrich]

Post by Stefan Ram

Post by Ralf Ullrich
Angenommen es gäbe eine Methode anhand eines Programmtextes zu
beweisen, dass ein Programm terminiert, dann müsste diese
Methode für das Beispielprogramm zwei gegensätzliche Ergebnisse
liefern, und das bei gleicher "Eingabe".

Einige bekannte Aussagen zum Halteproblem finden sich
http://de.wikipedia.org/wiki/Halteproblem
Du hast also noch einmal ein Beispiel dazu geliefert, das
wohl mit dem Bekannten (aus obigem Wikipädie-Artikel)
verträglich ist.

Naja, ich sehe es eigentlich mehr so, dass ich gezeigt habe, dass Java
nicht auf einer Turingmaschine implementierbar ist. Man darf nie
vergessen, dass "die Turingmaschine" nur ein theoretisches Modell für
einen Rechner ist, und dass heutige Rechner dieses Modell an vielen
Stellen nicht einhalten, vom offensichtlich nicht unendlichen Speicher mal
ganz abgesehen.

Wenn Java selbst nun nicht auf einer Turingmaschine implementierbar ist,
dann ist jegliche Theorie, die sich der Turingmaschine als Modell bedient
nur noch begrenzt auf Java übertragbar.

Post by Stefan Ram

Post by Ralf Ullrich
Mit der gleichen Antwort, die ihr hoffentlich alle auf dieses
Warum findet, kann man auch jeden Versuch die Korrektheit eines
nicht trivialen Java-Programms zu beweisen, von vornherein in
den Wind schlagen.

Man kann sich ja auf eine Teilmenge von Java beschränken,
bei der so etwas möglich ist.

Genau das machen ja die anfangs im Thread erwähnten Produkte, weshalb es
dann eigentlich unsinnig ist, diesen Produkten vorzuwerfen, dass sie nicht
alles prüfen können.

cu

[Michael Paap]

Post by Ralf Ullrich
Naja, ich sehe es eigentlich mehr so, dass ich gezeigt habe, dass Java
nicht auf einer Turingmaschine implementierbar ist. Man darf nie
vergessen, dass "die Turingmaschine" nur ein theoretisches Modell für
einen Rechner ist, und dass heutige Rechner dieses Modell an vielen
Stellen nicht einhalten, vom offensichtlich nicht unendlichen Speicher mal
ganz abgesehen.

Das ist ein Grund, warum man in Java keine Turingmaschine wirklich
komplett emulieren kann, aber kein Grund, warum Java nicht auf einer
(naturgemäß immer imaginären) Turingmaschine implementierbar sein sollte.

Gruß,
Michael

[Jochen Theodorou]

Post by Ralf Ullrich
Hi Jochen, Gerd, Wanja, etc.
Ich habe eure Diskussion nicht im Detail verfolgt, und zwar weil es
müssig ist für Java darüber zu disktuieren ob man die
Korrektheit/Terminierung eines Programms beweisen kann.
Anbei ein Beispiel für ein Java Programm, dass auf den meisten
Einprozessor-Rechnern, die Java Programme ausführen können beinahe
sofort terminiert, allerdings mit einem mehr oder weniger zufälligen
Ergebnis. (Und das liegt eigentlich nicht daran, dass java.util.Random
verwendet wird.)
Auf einem Mehrprozessorsystem hingegen wird dasselbe Program womöglich
ewig laufen.

nicht anders herum? Zudem kommt es auf die Anzhal der möglichen
parallelen Prozesse an, die dabei genutzt wird.

Gruss theo

[Ingo Menger]

Post by Ralf Ullrich
Hi Jochen, Gerd, Wanja, etc.
Ich habe eure Diskussion nicht im Detail verfolgt, und zwar weil es müssig
ist für Java darüber zu disktuieren ob man die Korrektheit/Terminierung
eines Programms beweisen kann.

Das mit der Terminierung ist ein Streit um des Kaisers Bart. Wenn man
irgendwelche Aussagen über Programme beweisen möchte, muß man sich
vorher ja mal überlegen, was für Aussagen das sein sollen. Ich denke,
es spricht vieles dafür, daß das nur Aussagen sein können, die in
der Programmiersprache selbst formulierbar sind. (Wäre dem nicht so,
hätte man eine formal verifizierbar sein sollende
Spezifizierungssprache, die offensichtlich mächtiger ist als die
Programmiersprache, aber wozu bräuchte man dann letztere noch?)
Ob das Programm terminiert oder nicht ist jedefalls eine Frage in einer
Metasprache und wie wir wissen, entzieht sich diese der automatischen
Entscheidbarkeit.

(Hingegen können Programme, die für was ganz anderes gedacht waren,
wie z.B. Typinferenzalgorithmen u.U. "nebenbei" erkennen, daß das
Programm nicht terminiert. Siehe als Beispiel
http://perl.plover.com/yak/typing/samples/slide027.html und folgende
Folien.)

[Gerd K.]

Hi!

Post by Jochen Theodorou
Ok, dann etwas formaler...
Sei c eine Anweiseung, sei v der Zustand des Systems
Es gilt v --c--> v', also c überführt ein bestimmtes v in v'. Ein
Programm bestehe nun aus einer Verkettung von cs, also "c1; c2; c3" usw.
Jedes c1 überführt v in v1, c2 überführt v1 in v2 usw. Sei cr der Rest
des noch auszuführenden Programmes. Sammele ich nun all diese (vi,cr1),
dann kann ich eine Endlosschleife dann feststellen, wenn sich ein
(vj,cr2) findet mit vj=v1 und cr1 = cr2. Das kann ich annehmen aufgrund
der Transitivität. Allein der Nichtdeterminismus kann hier einen Strich
durch die Rechnung machen.

Aber nicht jede Endlosschleife wird zu einem Zyklus führen.
Die reelle Zahl
0,010010001000010000010000001usw
hat unendlich viele Nachkommastellen, aber keine Periode...
Auch wenn ein Graph nur endlich viele Knoten hat, so gibt es doch
unendliche zyklenfreie Durchläufe.

Die Äquivalenz
Algorithmus terminiert nicht <=> Es gibt i,j, r1,r2 mit
(vi,cr1)=(vj,cr2)
gilt nicht. Es liegt "lediglich" eine Implikation in der
Richtung <= vor.

Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hi!

Post by Jochen Theodorou
Ok, dann etwas formaler...
Sei c eine Anweiseung, sei v der Zustand des Systems
Es gilt v --c--> v', also c überführt ein bestimmtes v in v'. Ein
Programm bestehe nun aus einer Verkettung von cs, also "c1; c2; c3" usw.
Jedes c1 überführt v in v1, c2 überführt v1 in v2 usw. Sei cr der Rest
des noch auszuführenden Programmes. Sammele ich nun all diese (vi,cr1),
dann kann ich eine Endlosschleife dann feststellen, wenn sich ein
(vj,cr2) findet mit vj=v1 und cr1 = cr2. Das kann ich annehmen aufgrund
der Transitivität. Allein der Nichtdeterminismus kann hier einen Strich
durch die Rechnung machen.

Aber nicht jede Endlosschleife wird zu einem Zyklus führen.
Die reelle Zahl
0,010010001000010000010000001usw
hat unendlich viele Nachkommastellen, aber keine Periode...
Auch wenn ein Graph nur endlich viele Knoten hat, so gibt es doch
unendliche zyklenfreie Durchläufe.

wenn die relle Zahl dafür ein Beispiel sein soll, dann ist das kein
endlicher Graph, weil du ja sagst es gäbe unendliche viele
Nachkommastellen. Auch PI is im Computer endlich. sowas kannst du nicht
als Wiederlegung benutzen. Und für die Aussage dass ein Graph mit einer
endlichen Anzahl von Knoten unendlich viele zyklenfreie Durchläufe
existieren hätte ich gerne einen Beweis. Da jeder Knoten einen Zustand
kennzeichnet und bestimmte Zustände durch "c" in andere überführt werden
hast du immer einen gerichteten Graphen. Zyklenfrei bedeutet dass du
jeden Knoten maximal einmal besuchst. Wenn du aber jden Knoten nur
maximal einmal besuchst hat jeder Pfad eine endliche Länge. Und jetzt
erkläre mir bitte, wie in einem zyklenfreien Graphen in dem alle Pfade
eine endliche länge haben und es nur endliche viele Knoten gibt
unendlich viele Pfade existieren können... ich sage es können nicht mehr
als n! Pfade sein, denn vorrausgestzt alle Knoten im Graph sind
vollständig miteinander verbunden, dann kann ich vom ersten Knoten (n-1)
mögliche Folgeknoten wählen, von dort dann (n-2), dann (n-3) usw. Also
(n-1)*(n-2)*(n-3)*...*(n-(n-1)) = (n-1)! Und n! ist immernoch endlich

Post by Gerd K.
Die Äquivalenz
Algorithmus terminiert nicht <=> Es gibt i,j, r1,r2 mit
(vi,cr1)=(vj,cr2)
gilt nicht. Es liegt "lediglich" eine Implikation in der
Richtung <= vor.

wie gesagt, dazu hätter ich gerne ein Gegenbeispiel, deine relle Zahl
ist keines. Ich bin leider nicht so gut im konstruieren von Beweisen,
sonst würde ich das kurz machen, aber ein Gegenbeispiel würde mir ja
schon reichen.

Und es ist nicht so wichtig zu wissen ob der Algorithmus in endlicher
Zeit vollendet wird, sondern, ob es Werte gibt für die das nicht der
Fall ist. Angenommen ich habe:

while (true) {
if (in.read()==5) break
}

Dann habe ich ja offensichtlich eine Endlosschleife für alle Werte von
in.read()!=5. Und genau das würde das Verfahren dann sagen. ob in.read
jemals eine eine 5 Liefert ist dann völlig belanglos. Es lässt sich
sogar ein naives Verfahren dafür bauen, das möglicherweise zu lange
braucht um etwas sinnvolles auszugeben, aber meiner Überzeugung nach
endlich ist.

Ich denke es dürfte äusserst schwierig sein ein Beispiel zu geben, wo
nur endliche Werte verwendet werden, aber keine Schleife dabei
herauskommen darf. Ich würde aber gerne so ein Beispiel sehen.

Gruss theo

[Gerd K.]

Hi!

Post by Jochen Theodorou
wenn die relle Zahl dafür ein Beispiel sein soll, dann ist das kein
endlicher Graph, weil du ja sagst es gäbe unendliche viele
Nachkommastellen. Auch PI is im Computer endlich.

Warum? Ich kann mir doch ein Programm schreiben, welches
pro Schleifendurchlauf die nächste Nachkommastelle von PI ausgibt...
Im Hexadezimalsystem kann man zu jeder natürlichen Zahl
n die n.te Nachkommastelle von PI berechnen, ohne Kenntnis über die
Vorgänger zu haben:
David Bailey, Peter B. Borwein and Simon Plouffe. On The Rapid
Computation Of Various Polylogarithmic
Constants. Mathematics of Computation, vol. 66, no. 218 (April 1997), S.
903-913 (Online verf¨ugbar
unter http://crd.lbl.gov/~dhbailey/dhbpapers/digits.pdf, Aufruf:
06.12.2004) 3, 11, 13
oder zur Einführung:
http://www-math.uni-paderborn.de/~aggathen/vorl/2004ws/sem/sebastian-aland.pdf

Post by Jochen Theodorou
sowas kannst du nicht
als Wiederlegung benutzen.

Warum nicht, s.o.

Post by Jochen Theodorou
Und für die Aussage dass ein Graph mit einer
endlichen Anzahl von Knoten unendlich viele zyklenfreie Durchläufe
existieren hätte ich gerne einen Beweis.

Ein unendlicher zyklenfreier Durchlauf reicht ja schon.

Nimm das PI-Beispiel:
n=1;
while B do
Berechne n.te Nachkommastelle von PI;
Gib n.te Nachkommastelle aus
n=n+1
end while;
für eine boolesche Bedingung B, die ich aufgenommen habe, damit der
Graph auch einen erreichbaren Endzustand bekommt.
Sowohl die Menge der Eingaben ( {} ) als auch die Menge der
Ausgaben pro Durchlauf {0,1...,9} sind endlich.

Zu diesen Algorithmus kann ich einen Graphen mit 11 Knoten angeben,
n_start, n_0 bis n_9 und n_stopp. Dieser Graph ist nicht zyklenfrei,
wohl aber der Durchlauf, der sich ergibt.

Post by Jochen Theodorou
Da jeder Knoten einen Zustand
kennzeichnet und bestimmte Zustände durch "c" in andere überführt werden
hast du immer einen gerichteten Graphen. Zyklenfrei bedeutet dass du
jeden Knoten maximal einmal besuchst.

Du sprichst von einen zyklenfreien Graphen, ich sprach von einem
unendlichen Weg durch den Graphen, den man nicht als Zyklus
identifizieren kann.

Post by Jochen Theodorou
Dann habe ich ja offensichtlich eine Endlosschleife für alle Werte von
in.read()!=5. Und genau das würde das Verfahren dann sagen. ob in.read
jemals eine eine 5 Liefert ist dann völlig belanglos. Es lässt sich
sogar ein naives Verfahren dafür bauen, das möglicherweise zu lange
braucht um etwas sinnvolles auszugeben, aber meiner Überzeugung nach
endlich ist.

Ich bezweifele nicht, dass sowas für eine Menge von Programmen
möglich ist oder sein wird, ich bezweifele, dass das i.A. geht.
Dein obiges Beispiel
while (true) {
if (in.read()==5) break
}
kann man ja sofort in
while (!in.read()==5) {
} umwandeln und direkt ablesen, wann eine Endlosschleife vorliegt.

Schwerer ist es hier:

LeseEin(zahl);
solange zahl<>1
zahl gerade? : zahl := zahl/2
zahl ungerade?: zahl := 3*zahl +1
end schleife

Für welche Eingaben terminiert die Schleife nicht?

Wer die Frage lösen kann, bekommt die Fields-Medaille, den Nobelpreis
der Mathematiker. Stichworte: Collatz conjecture, Ulam conjecture,
3n+1 conjecture

Aber jetzt sind wir wirklich weit weg vom Thema dieser Newsgruppe ;-)

Schönes Wochenende und Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hi!

Post by Jochen Theodorou
wenn die relle Zahl dafür ein Beispiel sein soll, dann ist das kein
endlicher Graph, weil du ja sagst es gäbe unendliche viele
Nachkommastellen. Auch PI is im Computer endlich.

Warum? Ich kann mir doch ein Programm schreiben, welches
pro Schleifendurchlauf die nächste Nachkommastelle von PI ausgibt...
Im Hexadezimalsystem kann man zu jeder natürlichen Zahl
n die n.te Nachkommastelle von PI berechnen, ohne Kenntnis über die

aber n ist endlich.

[...]

Post by Gerd K.

Post by Jochen Theodorou
sowas kannst du nicht als Wiederlegung benutzen.

Warum nicht, s.o.

Post by Jochen Theodorou
Und für die Aussage dass ein Graph mit einer
endlichen Anzahl von Knoten unendlich viele zyklenfreie Durchläufe
existieren hätte ich gerne einen Beweis.

Ein unendlicher zyklenfreier Durchlauf reicht ja schon.

Ein zyklus nimmt doch naturgemäß nur die Anzahl der Verfügbaren Knoten,
wenn diese Anzahl endlich ist, dann ist auch der Zyklus endlich...
zumindest wenn ich in so definieren, dass "Anfangsknoten" = "Endknoten"
gelten soll. Andernfalls gäbe es nur 2 Darstellungen, wovon die ein
endlich, die andere unendlich wäre.

Post by Gerd K.
n=1;
while B do
Berechne n.te Nachkommastelle von PI;
Gib n.te Nachkommastelle aus
n=n+1
end while;

und was machst für n hat einen grössten Wert den es erreichen kann.

Post by Gerd K.
für eine boolesche Bedingung B, die ich aufgenommen habe, damit der
Graph auch einen erreichbaren Endzustand bekommt.
Sowohl die Menge der Eingaben ( {} ) als auch die Menge der
Ausgaben pro Durchlauf {0,1...,9} sind endlich.
Zu diesen Algorithmus kann ich einen Graphen mit 11 Knoten angeben,
n_start, n_0 bis n_9 und n_stopp. Dieser Graph ist nicht zyklenfrei,
wohl aber der Durchlauf, der sich ergibt.

deine n_i sind aber keine Zustände.

Post by Gerd K.

Post by Jochen Theodorou
Da jeder Knoten einen Zustand
kennzeichnet und bestimmte Zustände durch "c" in andere überführt werden
hast du immer einen gerichteten Graphen. Zyklenfrei bedeutet dass du
jeden Knoten maximal einmal besuchst.

Du sprichst von einen zyklenfreien Graphen, ich sprach von einem
unendlichen Weg durch den Graphen, den man nicht als Zyklus
identifizieren kann.

Bitte zeige mir eine Aussage irgendwo, die Behauptet ein endlicher Graph
enthielte einen unendliche Pfad, und kein Teil dieses Pfades ist ein
Zyklus. Das übersteigt meine Vorstellungskraft komplett, denn um
irgendwas unendliches dort hinein zu bekommen müsstest du Knoten
mehrmals besuchen. Das hatten wir aber doch explizit ausgeschlossen, da
dies zu einem Zyklus führt.

Post by Gerd K.

Post by Jochen Theodorou
Dann habe ich ja offensichtlich eine Endlosschleife für alle Werte von
in.read()!=5. Und genau das würde das Verfahren dann sagen. ob in.read
jemals eine eine 5 Liefert ist dann völlig belanglos. Es lässt sich
sogar ein naives Verfahren dafür bauen, das möglicherweise zu lange
braucht um etwas sinnvolles auszugeben, aber meiner Überzeugung nach
endlich ist.

Ich bezweifele nicht, dass sowas für eine Menge von Programmen
möglich ist oder sein wird, ich bezweifele, dass das i.A. geht.
Dein obiges Beispiel
while (true) {
if (in.read()==5) break
}
kann man ja sofort in
while (!in.read()==5) {
} umwandeln und direkt ablesen, wann eine Endlosschleife vorliegt.
LeseEin(zahl);
solange zahl<>1
zahl gerade? : zahl := zahl/2
zahl ungerade?: zahl := 3*zahl +1
end schleife
Für welche Eingaben terminiert die Schleife nicht?

0 zum Beispiel ;) Was wäre denn wenn ich statt LeseEin(zahl) für zhal
einfach alle möglichen Werte ansetze? Mein erster Zustandknoten wäre
dann vor LeseZahl, davon ausgehen würden n zustandknoten mit dem
geänderten Wert für Zahl. Dann könnte man die Schleife durchlaufen,
wobei man jeden Zustand im Grphen protokolliert. stösst man dabei auf
einen bereits vorhandenen Knoten, dann gelten für die Ausgangszahl die
Bedingungen der Terminierung, so wie sie für diesen Knoten berechnet
wurden. Sobald also die Schleife einen bekannten Wert trifft, kann ich
eine Asusage über die Terminierung machen. Da es nur maximal n mögliche
Werte gibt für Zahl, kann ich nach n Durchläufen für eine bestimmte Zahl
sagen ob der Algorithmus termineirt. Für weitere Zahlen ist weniger
notwendig, weil die Zustände aus der vorherigen Berechnung mit genutzt
werden können.

z.B
z0 = Z(zahl = 0,solange...) -> Z(zahl=0,solange) == z0 -> terminiert nicht
z1 = Z(zahl=1,solange...) -> terminiert
z2 = Z(zahl=2,solange...) -> Z(zahl=1,solange) == z1 -> terminiert
z3 = Z(zahl=3,solange...) -> Z(zahl=10,solange) == z10, status
unbekannt. -> Z(zahl=5,..) = z5, status unbekannt ->
fürhrt zu 16, 8, 4, 2, 1 -> terminiert. Die Knoten
z3,z10,z5,z16,z8,z4,z2 bekommen den status terminiert.
z4 -> terminiert
z5 -> terminiert
z6 -> z3 -> terminiert
z7 -> z22 -> z11 -> z34 -> z17 -> z52 -> z26 -> z13 -> z40 -> z20 ->
z10 -> terminiert

usw...

Problematisch für den Algorithmus erweist sich eventuell der Überlauf
bei 3*Zahl+1. In Java bekommt man dann plötzlich eine negative Zahl,
aber für die Frage tes terminieren ist das ja eher nebensächlich.

Gruss theo

[Michael Paap]

Post by Jochen Theodorou
Bitte zeige mir eine Aussage irgendwo, die Behauptet ein endlicher Graph
enthielte einen unendliche Pfad, und kein Teil dieses Pfades ist ein
Zyklus. Das übersteigt meine Vorstellungskraft komplett, denn um
irgendwas unendliches dort hinein zu bekommen müsstest du Knoten
mehrmals besuchen. Das hatten wir aber doch explizit ausgeschlossen, da
dies zu einem Zyklus führt.

Gerd definiert Zyklus anders als du und ich.

Gruß, Michael

[Ralf Ullrich]

Post by Michael Paap

Post by Jochen Theodorou
Bitte zeige mir eine Aussage irgendwo, die Behauptet ein endlicher Graph
enthielte einen unendliche Pfad, und kein Teil dieses Pfades ist ein
Zyklus. Das übersteigt meine Vorstellungskraft komplett, denn um
irgendwas unendliches dort hinein zu bekommen müsstest du Knoten
mehrmals besuchen. Das hatten wir aber doch explizit ausgeschlossen, da
dies zu einem Zyklus führt.

Gerd definiert Zyklus anders als du und ich.

Vor allem redet Jochen von einem Graphen bei dem von jedem Knoten nur ein
oder kein Weg wegführt, während bei Gerd zwei oder mehr Wege wegführen
können. Daher kann Gerd unendlich viele Teil-Zyklen konstruieren, die sich
aber im Gesamtweg im Graphen nicht periodisch wiederholen. Allerdings hat
Gerd's Graph IMHO nichts mehr mit dem Zustandsgraphen eines Programmlaufs
auf einer (deterministischen) Maschine zu tun, von dem Jochen redet. Außer
natürlich Gerd redet von einer nichtdeterministischen Maschine, aber dann
müsste er eigentlich alle Pfaden gleichermaßen folgen, statt nur
willkürlich einem. Und er müsste beim ersten Auftreten eines Zyklus
entscheiden, dass das Programm nicht anhält, da er ja nicht garantieren
kann, dass dieser Zyklus nicht doch genauso wiederholt wird (denn alle
Pfade sind gleichberechtigt, also auch wieder der Zyklus).

Kurz und bündig: Jochen und Gerd reden schon seit einigen Posts aneinander
vorbei.

cu

[Gerd K.]

Hi!

Post by Jochen Theodorou

Post by Gerd K.
Warum? Ich kann mir doch ein Programm schreiben, welches
pro Schleifendurchlauf die nächste Nachkommastelle von PI ausgibt...
Im Hexadezimalsystem kann man zu jeder natürlichen Zahl
n die n.te Nachkommastelle von PI berechnen, ohne Kenntnis über die

aber n ist endlich.

Aus der Endlichkeit
der Zifferdarstellung einer natürlichen Zahl kann man doch
nicht auf die Endlichkeit der Menge der natürlichen Zahlen
schliessen...Den Algorithmus kann ich doch für beliebig viele
Zahlen durchspielen.
Das ist auch nicht mit Aufwand verbunden, da ich keinerlei "Gedächtnis"
brauche.

Post by Jochen Theodorou

Post by Gerd K.
n=1;
while B do
Berechne n.te Nachkommastelle von PI;
Gib n.te Nachkommastelle aus
n=n+1
end while;

und was machst für n hat einen grössten Wert den es erreichen kann.

Den gibt es nicht... Du musst "nur" eine geeignete Repräsentation der
natürlichen Zahlen wählen, so dass es keine Bereichsüberläufe geben
kann.

Anderes Beispiel, ein Klassiker aus der Berechenbarkeitstheorie, hier
der Typ2-Berechenbarkeit: Der Zustandsautomat des Algorithmus zum Testen
auf Teilbarkeit durch 3 besteht aus gerade einmal 3 Zuständen. Für
beliebig lange natürlichen Zahlen entscheidet er, ob diese Zahl durch
3 teilbar ist, indem er immer nur eine weitere Ziffer der
Dezimaldarstellung
beachtet. Warum sollte es hier ein "Größenproblem" geben?
(Für Interessierte: Die drei Zustände entsprechen den Restklassen
modulo 3. Restklassenarithmetik wird geschickt angewendet...)

Post by Jochen Theodorou

Post by Gerd K.
LeseEin(zahl);
solange zahl<>1
zahl gerade? : zahl := zahl/2
zahl ungerade?: zahl := 3*zahl +1
end schleife
Für welche Eingaben terminiert die Schleife nicht?

0 zum Beispiel ;) Was wäre denn wenn ich statt LeseEin(zahl) für zhal
einfach alle möglichen Werte ansetze? Mein erster Zustandknoten wäre
dann vor LeseZahl, davon ausgehen würden n zustandknoten mit dem
geänderten Wert für Zahl. Dann könnte man die Schleife durchlaufen,
wobei man jeden Zustand im Grphen protokolliert. stösst man dabei auf
einen bereits vorhandenen Knoten, dann gelten für die Ausgangszahl die
Bedingungen der Terminierung, so wie sie für diesen Knoten berechnet
wurden. Sobald also die Schleife einen bekannten Wert trifft, kann ich
eine Asusage über die Terminierung machen. Da es nur maximal n mögliche
Werte gibt für Zahl, kann ich nach n Durchläufen für eine bestimmte Zahl

Warum sollte es nur endlich viele Möglichkeiten geben? Das ist doch
gerade
aktueller Forschungsgegenstand. Für deinen Graphen gilt folgende
Äquivalenz:

Der Graph besitzt endlich viele Knoten <=> Die Schleife terminiert

Du hast lediglich das Problem verschoben. Warum sollte Dein Graph immer
endlich viele Knoten haben?

In der Theorie gibt es übrigens einen solchen von Dir skizzierten
Ansatz zum Nachweis der Terminierung, die Terminierungsfunktion.
Mit Hilfe dieser Funktion wird nach jedem Schleifendurchlauf eine
ganze Zahl erzeugt. So ensteht eine Folge ganzer Zahlen. Wenn man
zeigen kann, dass diese Folge streng monoton steigend ist und
eine oberer Schranke besitzt bzw. streng monton fallend und eine
untere Schranke hat, hat man die Endlichkeit der Folge und damit
die Terminierung bewiesen. Bilde Deine Zustände nach Z ab, und
Du hast genau diesen Ansatz.

Aber jetzt sind wir wirklich schon sehr off topic ;-)

Viele Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hi!

wie schon in einem anderen Teil erwähnt wurde reden wir aneinander
vorbei. Ich rede von einem Zustandsautomaten mit endlichen Zuständen.
Oder besser gesagt einer endlichen Anzahl von Zustaänden. Jeder Zustand
besteht aus einer oder mehreren endlichen Zahlen. Einen solchen
Automaten kennzeichnet, dass er deterministisch ist oder deterministisch
gemacht werden kann. Was du meinst weiss ich nicht.

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
Warum? Ich kann mir doch ein Programm schreiben, welches
pro Schleifendurchlauf die nächste Nachkommastelle von PI ausgibt...
Im Hexadezimalsystem kann man zu jeder natürlichen Zahl
n die n.te Nachkommastelle von PI berechnen, ohne Kenntnis über die

aber n ist endlich.

Aus der Endlichkeit
der Zifferdarstellung einer natürlichen Zahl kann man doch
nicht auf die Endlichkeit der Menge der natürlichen Zahlen
schliessen...

hab ich auch nicht. Aber du kannst nur endliche Zahlen im Computer
benutzen. Selbst wenn du die nte Ziffer immer nur ausgibst hast du doch
irgendwo einen Zustand den du speichern musst. Diesen ZUstand speicherst
du entweder in Form eines Wertes oder durch die Struktur des Programmes.
Da aber auch die Größe des Programmes in einem Computer endlich ist hast
du keine Chance etwas unendliches darzustellen ausser durch eine
Schleife mit sich wiederholenden Zuständen. Und genau dieser Fall ist
der Fall der Endlosschleife, den ich ja erkennen wollte.

Post by Gerd K.
Den Algorithmus kann ich doch für beliebig viele
Zahlen durchspielen.

nur endlich viele!

Post by Gerd K.
Das ist auch nicht mit Aufwand verbunden, da ich keinerlei "Gedächtnis"
brauche.

Falsch. Entweder Gedächtnis, oder Endlosschleife. Ein Beispiel sind
vielleicht Pseudozufallszahlengeneratoren. Sie erzeugen scheinbare
Zufallszahlen, allerdings nicht unendlich viele. Nach einer gewissen
Zeit wiederholen sich die Zahlen. Ergo, Schleife.

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
n=1;
while B do
Berechne n.te Nachkommastelle von PI;
Gib n.te Nachkommastelle aus
n=n+1
end while;

und was machst für n hat einen grössten Wert den es erreichen kann.

Den gibt es nicht... Du musst "nur" eine geeignete Repräsentation der
natürlichen Zahlen wählen, so dass es keine Bereichsüberläufe geben
kann.

Die gibt es nicht wenn du nur endliche Dinge hast.

Post by Gerd K.
Anderes Beispiel, ein Klassiker aus der Berechenbarkeitstheorie, hier
der Typ2-Berechenbarkeit: Der Zustandsautomat des Algorithmus zum Testen
auf Teilbarkeit durch 3 besteht aus gerade einmal 3 Zuständen. Für
beliebig lange natürlichen Zahlen entscheidet er, ob diese Zahl durch
3 teilbar ist, indem er immer nur eine weitere Ziffer der
Dezimaldarstellung
beachtet. Warum sollte es hier ein "Größenproblem" geben?

Das Programm arbeitet auf einer unendlichen Eingabe, das ist eine völlig
andere Klasse, als das was ich hier betrachten wollte.

[...]

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
LeseEin(zahl);
solange zahl<>1
zahl gerade? : zahl := zahl/2
zahl ungerade?: zahl := 3*zahl +1
end schleife
Für welche Eingaben terminiert die Schleife nicht?

0 zum Beispiel ;) Was wäre denn wenn ich statt LeseEin(zahl) für zhal
einfach alle möglichen Werte ansetze? Mein erster Zustandknoten wäre
dann vor LeseZahl, davon ausgehen würden n zustandknoten mit dem
geänderten Wert für Zahl. Dann könnte man die Schleife durchlaufen,
wobei man jeden Zustand im Grphen protokolliert. stösst man dabei auf
einen bereits vorhandenen Knoten, dann gelten für die Ausgangszahl die
Bedingungen der Terminierung, so wie sie für diesen Knoten berechnet
wurden. Sobald also die Schleife einen bekannten Wert trifft, kann ich
eine Asusage über die Terminierung machen. Da es nur maximal n mögliche
Werte gibt für Zahl, kann ich nach n Durchläufen für eine bestimmte Zahl

Warum sollte es nur endlich viele Möglichkeiten geben?

Weil ich das so vorrausgestzt habe? Siehe oben.

Post by Gerd K.
Das ist doch gerade
aktueller Forschungsgegenstand. Für deinen Graphen gilt folgende
Der Graph besitzt endlich viele Knoten <=> Die Schleife terminiert

Nein! Der Graph hat immer endlich viele Knoten. Das bedeutet nicht das
die Schleife imm terminiert. Meine Aussage war, dass der Algorithmus
terminiert wenn der Graph frei von Zyklen ist, weil das eine
Endlosschleife wäre.

Post by Gerd K.
Du hast lediglich das Problem verschoben. Warum sollte Dein Graph immer
endlich viele Knoten haben?

Siehe oben.

Post by Gerd K.
In der Theorie gibt es übrigens einen solchen von Dir skizzierten
Ansatz zum Nachweis der Terminierung, die Terminierungsfunktion.
Mit Hilfe dieser Funktion wird nach jedem Schleifendurchlauf eine
ganze Zahl erzeugt. So ensteht eine Folge ganzer Zahlen. Wenn man
zeigen kann, dass diese Folge streng monoton steigend ist und
eine oberer Schranke besitzt bzw. streng monton fallend und eine
untere Schranke hat, hat man die Endlichkeit der Folge und damit
die Terminierung bewiesen. Bilde Deine Zustände nach Z ab, und
Du hast genau diesen Ansatz.

Mag sein, aber wie gesagt, ich sprach von reell existierenden Werten,
diese sind folglich endlich. Ein Programm das auf einer unendlichen
Eingabe arbeitet und jede Eingabestelle verarbeiten muss terminiert
natürlich nicht. Aber mein Graph enthält die Eingabe im Zustand, weil
aber alle Zustände bei mir endlich sein müssen ist es nicht möglich ein
solches Programm in meinem Modell zu analysieren. Trotzdem gilt auch
hier, dass die grösse meiens Programmes endlich sein muss, folglich kann
der Teil, der die unendliche Eingabe behandelt nicht uinendlich gross
sein. Damit das Programm aber die komplette Eingabe abarbeiten kann muss
es irgendwo eine Schleife geben.


Gruss theo

[Gerd K.]

Post by Jochen Theodorou

Post by Gerd K.
Den gibt es nicht... Du musst "nur" eine geeignete Repräsentation der
natürlichen Zahlen wählen, so dass es keine Bereichsüberläufe geben
kann.

Die gibt es nicht wenn du nur endliche Dinge hast.

Existiert die Zahl 2^1000000000000 nicht, nur weil man die
Dezimaldarstellung wegen der Begrenztheit der Atomanzahl im Universum
nicht aufschreiben kann? Kann man mit ihr nicht rechnen?
2*2^1000000000000=2^1000000000001
Es gibt so viele Eigenschaften dieser Zahl, die man benutzen kann,
ohne die Dezimaldarstellung zu kennen...

So etwas wie unendliche Zahlen gibt es nicht.

Da wir schon sehr offtopic sind, und sich kein anderer
für die Diskussion interessiert, sollten wir sie beenden.
100% werden wir uns nicht einigen können ;-)

Grüße!

[Jochen Theodorou]

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
Den gibt es nicht... Du musst "nur" eine geeignete Repräsentation der
natürlichen Zahlen wählen, so dass es keine Bereichsüberläufe geben
kann.

Die gibt es nicht wenn du nur endliche Dinge hast.

Existiert die Zahl 2^1000000000000 nicht,

Ich habe das Existenzrecht der DDR... ähm.. dieser Zahl nicht in Frage
gestellt ;)

Post by Gerd K.
nur weil man die
Dezimaldarstellung wegen der Begrenztheit der Atomanzahl im Universum
nicht aufschreiben kann? Kann man mit ihr nicht rechnen?
2*2^1000000000000=2^1000000000001
Es gibt so viele Eigenschaften dieser Zahl, die man benutzen kann,
ohne die Dezimaldarstellung zu kennen...

klar, darum geht es aber auch garnicht ;)

Post by Gerd K.
So etwas wie unendliche Zahlen gibt es nicht.

jein... Pi schient eine unendliche Zahl von Ziffern zu haben. Meine
Aussage lediglich in die Richtung, dass wenn ich die Validität eines
Algorithmus überprüfen will und dieser als Eingabe ein bate bekommt, ich
dann nicht die Werte eines ints berücksichtigen muss, sondern die des
byte. Und bytes haben nunmal nur 256 verschiedene Werte. Es gibt also
eine kleinste obere Grenze.

Post by Gerd K.
Da wir schon sehr offtopic sind, und sich kein anderer
für die Diskussion interessiert, sollten wir sie beenden.
100% werden wir uns nicht einigen können ;-)

Ja, ok... oder wir machen ein prost-Thread draus ;) Aber ich denke
nciiht dass da noch viel drin ist, weil ich dir das scheinbar nicht
erklären kann.

Gruss theo

[Gerd K.]

Hi!
Die letzte Antwort, versprochen ;-)

Post by Jochen Theodorou
jein... Pi schient eine unendliche Zahl von Ziffern zu haben. Meine
Aussage lediglich in die Richtung, dass wenn ich die Validität eines
Algorithmus überprüfen will und dieser als Eingabe ein bate bekommt, ich
dann nicht die Werte eines ints berücksichtigen muss, sondern die des
byte. Und bytes haben nunmal nur 256 verschiedene Werte. Es gibt also
eine kleinste obere Grenze.

Klar! Aber bei dem Collatz-Problem z.B. ist die Eingabe nach
Spezifikation
eine beliebige natürliche Zahl. Die Eingabemenge ist eben nicht
die größte auf dem Rechner xyz "speicherbare" Zahl...Und wenn man das
auf ein Programm abbildet, welches nur eine endliche Anzahl von
Eingabewerte erlaubt, hat man etwas falsch gemacht!

Post by Jochen Theodorou
Ja, ok... oder wir machen ein prost-Thread draus ;) Aber ich denke
nciiht dass da noch viel drin ist, weil ich dir das scheinbar nicht
erklären kann.

Wir sind hier mitten in dem uralten Grundlagenstreit zwischen den
Konstruktivisten und den echten Theoretikern ;-))
Meine persönliche Meinung: Die konstruktivistischen Einschränkungen
verhindern die ernsthafte, zeitlose Auseinandersetzung mit interessanten
Fragestellung und vermitteln eine etwas zu simple Sichtweise
auf viele Probleme. Wenn ich mich jetzt richtig erinnere, war es der
große Hilbert, der sinngemäß gesagt hat, dass die Konstruktivisten
versuchen, "uns aus dem Cantorschen Paradies zu vertreiben". *g*

Viele Grüße!

[Jochen Theodorou]

Post by Gerd K.
Hi!
Die letzte Antwort, versprochen ;-)

Post by Jochen Theodorou
jein... Pi schient eine unendliche Zahl von Ziffern zu haben. Meine
Aussage lediglich in die Richtung, dass wenn ich die Validität eines
Algorithmus überprüfen will und dieser als Eingabe ein bate bekommt, ich
dann nicht die Werte eines ints berücksichtigen muss, sondern die des
byte. Und bytes haben nunmal nur 256 verschiedene Werte. Es gibt also
eine kleinste obere Grenze.

Klar! Aber bei dem Collatz-Problem z.B. ist die Eingabe nach
Spezifikation
eine beliebige natürliche Zahl. Die Eingabemenge ist eben nicht
die größte auf dem Rechner xyz "speicherbare" Zahl...Und wenn man das
auf ein Programm abbildet, welches nur eine endliche Anzahl von
Eingabewerte erlaubt, hat man etwas falsch gemacht!

Der URsprung wr ja meine Behauptung, dass man ein jedes reales Program
in einen Zustandsgraphen überführen kann und wenn dieser Graph
zyklenfrei ist, dass das Programm dann terminiert. Vorraussetzung sind
ein endliches Programm, endliche Eingabe, sowie endliche Zustände. Ein
solcher Graph kann unter Umständen äusserst gross werden und ist daher
nicht unbedingt praxisrelevant. ich wollte damit nur andeuten unter
welchen Bediungungen das Halteproblem nun doch lösbar ist. Dass es im
allgemeinen nicht lösbar ist, ist mir klar und will ich hier auch
niemals bestritten haben.

Post by Gerd K.

Post by Jochen Theodorou
Ja, ok... oder wir machen ein prost-Thread draus ;) Aber ich denke
nicht dass da noch viel drin ist, weil ich dir das scheinbar nicht
erklären kann.

Wir sind hier mitten in dem uralten Grundlagenstreit zwischen den
Konstruktivisten und den echten Theoretikern ;-))
Meine persönliche Meinung: Die konstruktivistischen Einschränkungen
verhindern die ernsthafte, zeitlose Auseinandersetzung mit interessanten
Fragestellung und vermitteln eine etwas zu simple Sichtweise
auf viele Probleme. Wenn ich mich jetzt richtig erinnere, war es der
große Hilbert, der sinngemäß gesagt hat, dass die Konstruktivisten
versuchen, "uns aus dem Cantorschen Paradies zu vertreiben". *g*

Ich würde mich zu denen dazwischen zählen.

Gruss theo

[Bernd Eckenfels]

Post by Gerd K.
Zu diesen Algorithmus kann ich einen Graphen mit 11 Knoten angeben,
n_start, n_0 bis n_9 und n_stopp. Dieser Graph ist nicht zyklenfrei,
wohl aber der Durchlauf, der sich ergibt.

Wenn der Graph den internen Zustand angeben soll, dann kannst du das nicht.

Ich verstehe uebrigens nicht so ganz was CS 101 oder partielle Korrektheit
von Programmen mit dem Topic zu tun hat.

Gruss
Bernd

[Michael Paap]

Post by Gerd K.
Auch wenn ein Graph nur endlich viele Knoten hat, so gibt es doch
unendliche zyklenfreie Durchläufe.

Ähm, bitte wie? Habe ich irgendwelche neue Entwicklungen in der
Graphentheorie verpasst? *g*

Gruß,
Michael

[Gerd K.]

Hi!

Post by Michael Paap

Post by Gerd K.
Auch wenn ein Graph nur endlich viele Knoten hat, so gibt es doch
unendliche zyklenfreie Durchläufe.

Ähm, bitte wie? Habe ich irgendwelche neue Entwicklungen in der
Graphentheorie verpasst? *g*

Betrachte folgenden Graphen:

Knoten: n_0, n_1, n_stopp

Kanten: (n_0,n_0)
(n_0,n_1)
(n_1,n_0)
(n_1,n_stopp)
Start: n_0
Stopp-Knoten: n_stopp

Analog zu meinem Beispiel mit der reeelen Zahl
0,01001000100001usw.
wähle ich den Durchlauf
n_0,n_1,n_0,n_0,n_1....

Ich sprach von einem zyklenfreien Durchlauf, nicht von einem
zyklenfreien Graphen ;-)
In einem endlichen zyklenfreien Graphen existieren natürlich keine
unendlichen Durchläufe.

Grüße!

[Ingo Menger]

Post by Gerd K.

Post by Ingo Menger
Hat sie nicht vielmehr das Gegenteil bewiesen?

Nein. ;-)

Das Halteproblem kenne ich.
Nur kannst Du *diese* Eigenschaft einer Funktion in gängigen
Programmiersprachen gar nicht ausdrücken. Deshalb kannst Du sie auch
nicht als Nachbedingung formulieren. Jede Nachbedingung B muß
eigentlich gelesen werden als "Wenn die Funktion terminiert, dann B".
Ich will also gar nicht beweisen, daß das Programm hält, sondern nur,
was gilt, wenn es hält.

Post by Gerd K.

Post by Ingo Menger
Stichwort
http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
Eines Tages werden wir hinschreiben, was wir beweisen wollen
(Spezifikation), dann werden wir den Beweis (das Programm) hinschreiben
und einen automatischen Beweisverifizierer nachprüfen lassen, daß wir
keinen Fehler gemacht haben.

Das ist aber eine ganz andere Qualität als das Berechnen des Beweises
selber. Es geht doch gerade um das Finden eines solchen, nicht
um die Verifizierung, dass es auch ein Beweis ist.

Aufgrund des o.g. Isomorphismus könnte das aber auf dasselbe
hinauslaufen.
Wahrscheinlich wird nicht alles auf einmal gehen.
Derzeit kann man ziemlich leicht "beweisen", daß eine Funktion f
denundden Typ hat.
Demnächst wird man beweisen können (und aufgrund der
Hardwareentwicklung auch immer öfter wollen), daß ein paralleles
Programm keine Deadlocks hat.
Und so wird das hoffentlich weitergehen.
Ich bin ziemlich optimistisch, daß in 10 oder 20 Jahren keine
nennenswerten SW-Systeme mehr laufen werden, deren Spezifikation nicht
wenigstens teilweise formal verifiziert worden ist.

[Ingo Menger]

Post by Ingo Menger
Ich bin ziemlich optimistisch, daß in 10 oder 20 Jahren keine
nennenswerten SW-Systeme mehr laufen werden, deren Spezifikation nicht
wenigstens teilweise formal verifiziert worden ist.

Anmerkung dazu: Mit der UML 2 hat die OMG m.E. einen Schritt in die
Richtung gemacht. Plakativ gesagt, vom Malen lustiger, aber
unverbindlicher Bildchen mit kleinen Strichmännchen hin zu einer
überhaupt formal verifizierbaren Spezifikation ist ein Schritt
gegangen worden. Da ist natürlich noch viel zu tun, aber es läuft am
Ende darauf hinaus, daß die Spezifikation das Programm *ist*.

[Ingo R. Homann]

Hi,

Post by Ingo Menger
Anmerkung dazu: Mit der UML 2 hat die OMG m.E. einen Schritt in die
Richtung gemacht. Plakativ gesagt, vom Malen lustiger, aber
unverbindlicher Bildchen mit kleinen Strichmännchen hin zu einer
überhaupt formal verifizierbaren Spezifikation ist ein Schritt
gegangen worden. Da ist natürlich noch viel zu tun, aber es läuft am
Ende darauf hinaus, daß die Spezifikation das Programm *ist*.

...was das Problem aber keineswegs löst oder auch nur vereinfacht,
sondern nur verlagert.

Wie oft ruft der Kunde an und meldet einen Bug, der sich - nach etwas
"Debugging" - nicht als Bug, sondern als Feature ("Im Endeffekt wollten
Sie's ja genau so haben!") herausstellt! (*)

Das Erstellen einer 'korrekten' Spezifikation (oder besser 'sinnvollen
Spezifikation', denn 'korrekt' ist sie ja per Definition :-) ist eben
das Anspruchsvolle.

Ciao,
Ingo

(*) Was natürlich nicht heissen soll, dass man den Kundenwunsch
ignoriert. Aber man verändert (bzw. verfeinert) dann halt im Nachhinein
seine Spezifikation.

[Ingo Menger]

Post by Ingo R. Homann
Hi,

Post by Ingo Menger
Anmerkung dazu: Mit der UML 2 hat die OMG m.E. einen Schritt in die
Richtung gemacht. Plakativ gesagt, vom Malen lustiger, aber
unverbindlicher Bildchen mit kleinen Strichmännchen hin zu einer
überhaupt formal verifizierbaren Spezifikation ist ein Schritt
gegangen worden. Da ist natürlich noch viel zu tun, aber es läuft am
Ende darauf hinaus, daß die Spezifikation das Programm *ist*.

...was das Problem aber keineswegs löst oder auch nur vereinfacht,
sondern nur verlagert.
Wie oft ruft der Kunde an und meldet einen Bug, der sich - nach etwas
"Debugging" - nicht als Bug, sondern als Feature ("Im Endeffekt wollten
Sie's ja genau so haben!") herausstellt! (*)

In dem und anderen Fällen wäre es aber schon eine Erleichterung, wenn
Du nicht noch prüfen müßtest, inwieweit diverse manuell erstellte
Artefakte mit der Spezifikation übereinstimmen. Finde ich.

Post by Ingo R. Homann
Das Erstellen einer 'korrekten' Spezifikation (oder besser 'sinnvollen
Spezifikation', denn 'korrekt' ist sie ja per Definition :-) ist eben
das Anspruchsvolle.

ACK, bis auf das mit dem 'korrekt'. Ich bin überzeugt, daß heutzutage
so einiger Unsinn zusammenanalysiert und -designed wird. Bei der
Implementierung fällt das dann auf, und ein neuer Entwicklungszyklus
beginnt.
Ich denke aber, es wird schon sehr bald Tools im Alltag geben, die
gnadenlos Modelle als "unterspezifiziert", "mehrdeutig" oder
"widersprüchlich" aussondern.

[Ingo R. Homann]

Hi,

Post by Ingo Menger

Post by Ingo R. Homann
Wie oft ruft der Kunde an und meldet einen Bug, der sich - nach etwas
"Debugging" - nicht als Bug, sondern als Feature ("Im Endeffekt wollten
Sie's ja genau so haben!") herausstellt! (*)

In dem und anderen Fällen wäre es aber schon eine Erleichterung, wenn
Du nicht noch prüfen müßtest, inwieweit diverse manuell erstellte
Artefakte mit der Spezifikation übereinstimmen. Finde ich.

Nun, aber die Spezifikation muss doch auch manuell erstellt werden,
insofern ist nicht viel gewonnen...

Post by Ingo Menger

Post by Ingo R. Homann
Das Erstellen einer 'korrekten' Spezifikation (oder besser 'sinnvollen
Spezifikation', denn 'korrekt' ist sie ja per Definition :-) ist eben
das Anspruchsvolle.

ACK, bis auf das mit dem 'korrekt'. Ich bin überzeugt, daß heutzutage
so einiger Unsinn zusammenanalysiert und -designed wird. Bei der
Implementierung fällt das dann auf, und ein neuer Entwicklungszyklus
beginnt.

Oft fällt das in der Implementationsphase auf, oft aber auch nicht.

Mal ein Beispiel aus der Praxis, es ging um den Druck von Bescheiden für
Kindergarten-Beiträge (die von diversen "Berechnungsgrundlagen", wie dem
Gehalt der Eltern abhängen):

Kunde: "Es soll immer dann ein Bescheid ausgedruckt werden, wenn sich
der zu zahlende Beitrag ändert."

Softwarelieferant: "OK"

K (später): "Moment mal - da hat sich das Einkommen von jemandem
geändert, und es kommt kein Bescheid aus dem System"

S: "Ja. Das Einkommen hat sich geändert, aber die Einkommensstufe nicht.
Also hat sich auch der zu zahlende Beitrag nicht geändert."

K: "Achso, hmmm. Na gut - dann soll halt immer dann ein Bescheid
ausgegeben werden, wenn sich an der 'Berechnungsgrundlage' was ändert,
und nicht nur, wenn sich am Beitrag was ändert"

S: "OK"

K (später): "Ach übrigens - auf dem Bescheid sollen die
Berechnungsgrundlagen natürlich ausgegeben werden. Aus
datenschutzrechtlichen Gründen soll aber nicht das Gehalt exakt
ausgegeben werden, sondern nur die Gehalts-Stufe."

S: "OK"

K: "He moment mal - hier ist ein Bescheid rausgekommen, auf dem hat sich
ja gar nichts geändert."

S: "Ja. Das liegt daran, dass immer dann ein Bescheid rauskommen sollte,
wenn sie die Berechnungsgrundlagen geändert haben. Die haben sich auch
geändert, nämlich in Form eines anderen Einkommens. Das Einkommen soll
ja aber nicht ausgegeben werden, sondern nur die Einkommensstufe - und
die wiederum hat sich nicht geändert."

K: "Achso, hmmm. Na gut - dann soll also immer dann ein Bescheid
gedruckt werden, wenn entweder sich die Einkommens*stufe* geändert hat,
oder wenn sich eine andere Berechnungsgrundlage als das Einkommen
geändert hat."

S: "OK."

K (später): "Ein Beitragszahler hatte anfangs sein Einkommen nicht
angegeben. Dadurch wird er ja (korrekterweise) in die höchste
Einkommensstufe eingruppiert. Jetzt hat er es doch angegeben, in der
Hoffnung, weniger zahlen zu müssen. Tatsählich liegt er aber wirklich in
der höchsten Einkommensstufe. Da ist jetzt aber kein Bescheid
rausgekommen. Wieso?"

S: "Weil Sie es genau so spezifiziert hatten - an der Einkommensstufe
("höchste") hat sich nichts geändert, an den anderen
Berechnungsgrundlagen hat sich auch nichts geändert und am Beitrag hat
sich auch nichts geändert!"

K: "Achso, hmmm. Gut, also in diesem Spezialfall soll aber dann also
doch ein Bescheid raus kommen!"

S: "OK"

Fortsetzung folgt.

Für's Protokoll: Ein paar der Dinge hatte der Softwarelieferant
tatsächlich vorausgesehen, so dass es sich der Dialog nicht wörtlich so
abgespielt hat - aber dieses Hin und Her hat es schon gegeben.

Ich denke, das zeigt sehr gut, wie schwierig es ist, eine Spezifikation
zu finden, die in der Praxis tauglich ist.

Post by Ingo Menger
Ich denke aber, es wird schon sehr bald Tools im Alltag geben, die
gnadenlos Modelle als "unterspezifiziert", "mehrdeutig" oder
"widersprüchlich" aussondern.

Das hätte in dem obigen Fall überhaupt nichts gebracht. Alle
Zwischenstufen der Spezifikation waren vollständig, nicht mehrdeutig und
auch nicht widersprüchlich.

Ciao,
Ingo

[Ingo Menger]

Post by Ingo R. Homann
Hi,

Post by Ingo Menger

Post by Ingo R. Homann
Wie oft ruft der Kunde an und meldet einen Bug, der sich - nach etwas
"Debugging" - nicht als Bug, sondern als Feature ("Im Endeffekt wollten
Sie's ja genau so haben!") herausstellt! (*)

In dem und anderen Fällen wäre es aber schon eine Erleichterung, wenn
Du nicht noch prüfen müßtest, inwieweit diverse manuell erstellte
Artefakte mit der Spezifikation übereinstimmen. Finde ich.

Nun, aber die Spezifikation muss doch auch manuell erstellt werden,
insofern ist nicht viel gewonnen...

Aber die Artefakte nicht mehr, bzw. nicht mehr manuell.

Post by Ingo R. Homann

Post by Ingo Menger

Post by Ingo R. Homann
Das Erstellen einer 'korrekten' Spezifikation (oder besser 'sinnvollen
Spezifikation', denn 'korrekt' ist sie ja per Definition :-) ist eben
das Anspruchsvolle.

ACK, bis auf das mit dem 'korrekt'. Ich bin überzeugt, daß heutzutage
so einiger Unsinn zusammenanalysiert und -designed wird. Bei der
Implementierung fällt das dann auf, und ein neuer Entwicklungszyklus
beginnt.

Oft fällt das in der Implementationsphase auf, oft aber auch nicht.

Um so schlimmer.

Post by Ingo R. Homann
Mal ein Beispiel aus der Praxis, es ging um den Druck von Bescheiden für
Kindergarten-Beiträge (die von diversen "Berechnungsgrundlagen", wie dem

[köstliches Beispiel gelöscht]

:)
Warum nur kommt mir das irgendwie so bekannt vor ...

Post by Ingo R. Homann
Ich denke, das zeigt sehr gut, wie schwierig es ist, eine Spezifikation
zu finden, die in der Praxis tauglich ist.

Allerdings.
Im Prinzip spielt sich hier die Geschichte "Der Computer macht nur, was
man ihm sagt: garbage in, garbage out." auf dem höheren
Abstraktionsniveau "Der Softwarepartner macht Ihnen nur, was Sie
verlangt haben." wieder ab.

Post by Ingo R. Homann

Post by Ingo Menger
Ich denke aber, es wird schon sehr bald Tools im Alltag geben, die
gnadenlos Modelle als "unterspezifiziert", "mehrdeutig" oder
"widersprüchlich" aussondern.

Das hätte in dem obigen Fall überhaupt nichts gebracht. Alle
Zwischenstufen der Spezifikation waren vollständig, nicht mehrdeutig und
auch nicht widersprüchlich.

Das stimmt.
(Insofern hatte Dein Beispiel nicht ganz das getroffen, was ich gemeint
hatte.)
Trotzdem, je mehr Anwendungssoftware zur "Wegwerfware" wird, bzw. eben
ständigen Änderungen und Weiterentwicklugen unterliegt, desto
wichtiger ist m.E. Toolsupport schon in ganz frühen Phasen und das
Automatisieren möglichst vieler Abschnitte des Entwicklungszyklus.

[Ingo R. Homann]

Hi,

Post by Ingo Menger

Post by Ingo R. Homann
Mal ein Beispiel aus der Praxis, es ging um den Druck von Bescheiden für
Kindergarten-Beiträge (die von diversen "Berechnungsgrundlagen", wie dem

[köstliches Beispiel gelöscht]
:)
Warum nur kommt mir das irgendwie so bekannt vor ...

Wahrscheinlich, weil das gang und gäbe ist.

Post by Ingo Menger

Post by Ingo R. Homann
Ich denke, das zeigt sehr gut, wie schwierig es ist, eine Spezifikation
zu finden, die in der Praxis tauglich ist.

Allerdings.
Im Prinzip spielt sich hier die Geschichte "Der Computer macht nur, was
man ihm sagt: garbage in, garbage out." auf dem höheren
Abstraktionsniveau "Der Softwarepartner macht Ihnen nur, was Sie
verlangt haben." wieder ab.

Nun, wie gesagt hat es sich nicht *exakt* so abgespielt - "der
Softwarepartner" war nämlich so schlau, dem Kunden das Szanario
(zumindest zu großen Teilen) schon im Voraus so auszumalen. Im Endeffakt
ist ja (u.a) auch genau das seine Aufgabe.

Trotzdem kommt so etwas wie das oben beschriebene doch sehr häufig vor.
(Vor allem, wenn der Kunde die Spezifikation zu kompliziert findet und -
zunächst - auf die "einfache" Spezifikation beharrt. ;-)

Post by Ingo Menger

Post by Ingo R. Homann
Das hätte in dem obigen Fall überhaupt nichts gebracht. Alle
Zwischenstufen der Spezifikation waren vollständig, nicht mehrdeutig und
auch nicht widersprüchlich.

Das stimmt.
(Insofern hatte Dein Beispiel nicht ganz das getroffen, was ich gemeint
hatte.)
Trotzdem, je mehr Anwendungssoftware zur "Wegwerfware" wird, bzw. eben
ständigen Änderungen und Weiterentwicklugen unterliegt, desto
wichtiger ist m.E. Toolsupport schon in ganz frühen Phasen und das
Automatisieren möglichst vieler Abschnitte des Entwicklungszyklus.

Ich glaube nicht, das so etwas jemals kommt (das wurde in regelmäßigen
Abständen seit mindestens 20 Jahren - oder sogar noch länger - erzählt)...

Ciao,
Ingo

[Ingo Menger]

Post by Ingo R. Homann
Hi,

Post by Ingo Menger
Trotzdem, je mehr Anwendungssoftware zur "Wegwerfware" wird, bzw. eben
ständigen Änderungen und Weiterentwicklugen unterliegt, desto
wichtiger ist m.E. Toolsupport schon in ganz frühen Phasen und das
Automatisieren möglichst vieler Abschnitte des Entwicklungszyklus.

Ich glaube nicht, das so etwas jemals kommt (das wurde in regelmäßigen
Abständen seit mindestens 20 Jahren - oder sogar noch länger - erzählt)...

Gegen Glauben kann ich natürlich nichts ausrichten ... :)
Aber man darf die Fortschritte, die in den 20 Jahren erzielt wurden,
nicht übersehen.
Und es zeichnen sich beispielsweise im MDA-Bereich schon ganz
hoffnungsvolle Ansätze ab. Für bestimmte Domänen gibt es bereits
(kommerziell verfügbare) Tools, bei denen "die Dokumentation der Code"
ist. Es ist dann z.B. nicht mehr nötig, den UML-Editor zu verlassen,
um einen Webservice zusammenzuklopfen.

[Gerd K.]

Post by Ingo R. Homann
Das Erstellen einer 'korrekten' Spezifikation (oder besser 'sinnvollen
Spezifikation', denn 'korrekt' ist sie ja per Definition :-) ist eben
das Anspruchsvolle.

110% Zustimmung! ;-)

Das Erarbeiten der Kundenwünsche ist mit das Anspruchsvollste und
ohne Frage das Wichtigste, was im Prozess der Softwareerstellung
gemacht wird. Nicht ohne Grund gibt es dafür eine eigene
Teildisziplin, das Requirements Engineering. Hier gemachte Fehler
sind die teuersten...

Was die Komplexität der Tätigkeit der Anforderungsermittlung
deutlich erhöht, ist der Kunde ;-) Dieser muss die Anforderungen
validieren! Dazu müssen sie aber auf einem Abstraktionsniveau
vorliegen, die der Kunde verstehen kann. Andererseits muss die
Anforderungsermittlung so formal sein, dass sie der Ausgangs-
punkt der weiteren Softwareentwicklung bildet und als
Vertragsgegenstand in das Pflichtenheft einfliessen kann...

Vorgehensmodelle, die keinen großen Wert auf eine vollständige
Anforderungsermittlung legen, sind mir sehr suspekt. Auch und gerade XP

Barry Boehm hat den Hype um sogenannte agile Vorgehensmodelle sehr
treffend charakterisiert, indem er aufzeigt, dass es bislang keine
Validierung solcher Modelle gibt, da die veröffentlichten Fallstudien
alle denselben Fehler haben: Die Entwicklergruppe bearbeitete
ein Problem aus einer schon bekannten Domäne, oft war es ein
Problem, welches diese Gruppe schon "klassisch" bearbeitet hatte.

Grüße!

[Daniel Thoma]

Das Halteproblem ist nicht der (direkte) Grund, warum jede Art von
Verifikation im _Allgemeinen_ nicht funktioniert. Der Grund ist vielmehr
der Satz von Rice (http://de.wikipedia.org/wiki/Satz_von_Rice), der
Besagt, dass keine (nicht triviale) Eigenschaft von Programmen
entscheidbar ist.
Wenn es also keinen mächtigeren Berechenbarkeitsbegriff als
Turing-Berechenbarkeit gibt (was anzunehmen ist), dann wird es auch nie
einen (vollständigen) Programmverifizierer geben.
Nun ist es aber so, dass man natürlich trotzdem in vielen Fällen
automatisch Eigenschaften von Programmen beweist. (Compiler Abwesenheit
von Typfehlern, der Java Bytecode Verifier Abwesenheit von unzulässigen
Stackzugriffen u.ä)

Es genügt also oft, eine Eigenschaft für eine Teilmenge der Programme
die sie erfüllen, beweisen zu können. Techniken in dem Bereich sind z.B.:
Typsysteme, Modell Checking, Abstrakte (überapproximierende) Semantiken.
Außerdem gibt es auch noch interaktive Beweissysteme, die nur Teile des
Beweises automatisch finden und den Beweis anschließend prüfen.

Es ist also durchaus Möglich, in einigen Fällen Verifikation zu
verwenden und es ist auch möglich, dass das irgendwann auch für normale
Anwendungssoftware nicht mehr zu aufwendig ist.
Allerdings ist natürlich erstmal eine formale Spezifikation erforderlich
und der Aufwand eine solche zu erstellen, lohnt sich wohl nur für
Software, die sehr Zuverlässig sein muss.

Irgendjemand hat zur UML 2.0 angemerkt, dass dort Zusicherungen möglich
sind und dass in Zukunft das Programm praktisch die Spezifikation sei.
Solche Zusicherungen eignen sich aber nur zur Verifikation, für
Überprüfungen zur Laufzeit oder für Testfälle. Es ist aber nicht
möglich, daraus automatisch Code zu generieren.

Grüße

Daniel

[Ingo Menger]

Post by Daniel Thoma
Irgendjemand hat zur UML 2.0 angemerkt, dass dort Zusicherungen möglich
sind und dass in Zukunft das Programm praktisch die Spezifikation sei.
Solche Zusicherungen eignen sich aber nur zur Verifikation, für
Überprüfungen zur Laufzeit oder für Testfälle. Es ist aber nicht
möglich, daraus automatisch Code zu generieren.

Das war ich.
Es ist mir klar, daß wir derzeit noch weit davon entfernt sind (außer
in Teilbereichen), daß die Spezifikation das Programm ist (nicht
umgekehrt).
Was OCL betrifft, so ist das eine hübsche kleine funktionale
Programmiersprache. Und natürlich köönte man schon heute aus
geigneten Vor- und Nachbedingungen Code generieren, der dafür sorgt,
daß die Nachbedingungen eingehalten sind.

Beispiel (in intuitiver Notation, habe jetzt OCL nicht im Kopf):

class Foo
+counter: Integer;
+ method inc()
pre: counter < MAX_INT
post: counter == pre.counter+1

Ist das schwer, daraus
void inc() { if (counter < MAX_INT) counter++; else throw new
PreConditionViolated(); }
zu generieren?

Natürlich sind nicht alle Fälle so einfach, aber letztlich
funktionieren ausgewachsene funktionale Sprachen auch nicht viel
anders. Im Prinzip schreibt man recht deklarativ nur den Ausdruck hin,
den man berechnet haben will.

[Daniel Thoma]

Ich habe mich mit OCL nicht genau beschäftigt und kenne nur andere
Spezifikationssprachen genauer.
Aber es ist ja schon klar, dass für eine Vorbedingung A, Nachbedingung B
und Programm P, nicht automatisch bewiesen werden kann, dass B nach P
gilt wenn zuvor A gilt. Du willst jetzt auch noch P suchen. Im
allgemeinen gibt es auch noch beliebig viele Lösungen, davon vor allem
auch sehr viel unbrauchbare, weil sie viel zu einfach sind.
Dein Beispiel ist offensichtlich, weil die Nachbedingung direkt die
Rechenvorschrift beschreibt.
Was aber wäre mit sowas:
Funktion: sort(A)
Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: \forall A_i, A_j, i < j; A_i < A_j

Diese Bedingung spezifiziert die Sortierung eines Arrays ohne doppelte
Elemente. Erwartest Du nun, dass da automatisch ein (guter)
Sortieralgorithmus gefunden wird?

Post by Ingo Menger
Natürlich sind nicht alle Fälle so einfach, aber letztlich
funktionieren ausgewachsene funktionale Sprachen auch nicht viel
anders.

Funktionale Sprachen funktionieren anders als typische
Spezifikationssprachen. Auch in funktionalen Sprachen wird im Prinzip
der Ablauf des Programms beschrieben, wenn auch nicht alle Ausdrücke so
ausgeführt werden, wie sie da stehen, um eine effizientere Ausführung
oder so Sachen wie endlos rekursive Datenstrukturen zu erlauben.
Aber es gibt auf jeden Fall direkt eine Vorschrift, wie man so ein
Programm interpretieren muss.
Logische Programmiersprachen gehen noch am ehesten in diese Richtung.
Aber da ist die verwendete Logik entsprechend eingeschränkt, damit das
funktioniert.

[Ingo Menger]

Post by Daniel Thoma
Ich habe mich mit OCL nicht genau beschäftigt und kenne nur andere
Spezifikationssprachen genauer.

Ich hab es auch nur gelesen, noch nicht verwendet.

Post by Daniel Thoma
Aber es ist ja schon klar, dass für eine Vorbedingung A, Nachbedingung B
und Programm P, nicht automatisch bewiesen werden kann, dass B nach P
gilt wenn zuvor A gilt.

Exakt: Es ist nicht wahr, daß für alle {A,B,P} bewisen werden kann,
daß ...
Aber: es existieren Triple {A,B,P} für die das bewiesen werden kann.
Vor allem dann, wenn man es hinkriegt, daß P als Beweis gelesen werden
kann, und nur noch überprüft werden braucht.

Post by Daniel Thoma
Du willst jetzt auch noch P suchen. Im
allgemeinen gibt es auch noch beliebig viele Lösungen, davon vor allem
auch sehr viel unbrauchbare, weil sie viel zu einfach sind.

Bedenkenswerter Punkt.

Post by Daniel Thoma
Dein Beispiel ist offensichtlich, weil die Nachbedingung direkt die
Rechenvorschrift beschreibt.
Funktion: sort(A)
Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: \forall A_i, A_j, i < j; A_i < A_j
Diese Bedingung spezifiziert die Sortierung eines Arrays ohne doppelte
Elemente.

Nein, das ist völlig unterspezifiziert. P könnte hier einfach [i..j]
lauten (d.h. der Aufruf einer Funktion, die ein Array mit Elementen i,
i+1, i+2, ..., j erzeugt).

Post by Daniel Thoma
Erwartest Du nun, dass da automatisch ein (guter)
Sortieralgorithmus gefunden wird?

Nein. Da müßtest Du schon genauer spezifizieren.
Aber ich schreib mal hin, wie die "Nachbedingung" aussehen könnte:

sort A
pre: /* A is an array */
post: result == merge (sort erste-hälfte) (sort zweite_hälfte)
where erste_hälfte = // konstruiere eine Hälfte
zweite_hälfte = // konstruiere andere Häkfte
merge A B = // mische zwei sortieite Arrays

Wie Du siehst. ist es absolut trivial, aus der Nachbedingung B P
abzuleiten.

Post by Daniel Thoma

Post by Ingo Menger
Natürlich sind nicht alle Fälle so einfach, aber letztlich
funktionieren ausgewachsene funktionale Sprachen auch nicht viel
anders.

Funktionale Sprachen funktionieren anders als typische
Spezifikationssprachen.

Das muß nicht so bleiben. Ich erwähnte funktionale Sprachen nur
deshalb, weil a) OCL m.E. eine (wenn auch noch eingeschränkte) ist und
b) weil in dem Bereich in punkto "automatic reasoning" seit Jahren
forschungsmäßig der Bär abgeht.

Post by Daniel Thoma
Auch in funktionalen Sprachen wird im Prinzip
der Ablauf des Programms beschrieben,

Ja schon, nur ist es eben absolut trivial, einen solchen Ablauf als
Nachbedingung umzuformulieren, indem ich für einen Ausdruck x, der den
"Ablauf" beschreibt immer
result == x schreibe. Siehe oben.

[Daniel Thoma]

Post by Ingo Menger
Nein, das ist völlig unterspezifiziert.

Das einzige, was fehlt, ist, dass hinterher die gleichen Elemente im
Array sein sollten. Man müsste also so etwas schreiben:

Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: (\forall A'_i, A'_j, i < j; A'_i < A'_j) && (\forall A_i
\exists j: A_i = A'_j && |A| = |A'|)
Der ' bedeutet, dass es sich um den Zustand nach der Ausführung handelt.
Damit ist also ausgedrückt, dass man ein Array will, das gleich lang
ist, das alle Elemente enthält und das sortiert ist.

Post by Ingo Menger
Nein. Da müßtest Du schon genauer spezifizieren.
sort A
pre: /* A is an array */
post: result == merge (sort erste-hälfte) (sort zweite_hälfte)
where erste_hälfte = // konstruiere eine Hälfte
zweite_hälfte = // konstruiere andere Häkfte
merge A B = // mische zwei sortieite Arrays

Das ist keine Spezifikation, das ist ein Algorithmus. Deine
Nachbedingung ist hier also, das Ergebnis soll das Ergebnis von
Mergesort sein. Es genügt aber einfach anzugeben, wie man überprüft,
dass ein Array sortiert ist. (Das ist, was ich gemacht habe.) Das
Beispiel Sortierung habe ich natürlich gewählt, weil es sehr einfach
ist, zu prüfen, dass ein Array sortiert ist.

Post by Ingo Menger
Das muß nicht so bleiben. Ich erwähnte funktionale Sprachen nur
deshalb, weil a) OCL m.E. eine (wenn auch noch eingeschränkte) ist und
b) weil in dem Bereich in punkto "automatic reasoning" seit Jahren
forschungsmäßig der Bär abgeht.

Es mag sein, dass man logische Sprachen bauen kann, in denen mehr geht,
als in heutigen logischen Sprachen. Aber OCL kann definitiv Vor- und
Nachbedingungen beschreiben, zu denen man im Allgemeinen automatisch
keine (gute) Lösung finden kann.
Man kann natürlich einfach den Lösungsraum aufzählen und immer die
Nachbedingung prüfen. Da man nur aufzählbare Ausgabemengen hat, muss man
dabei die Lösung finden (wenn es eine gibt). Aber das ist ja kein
brauchbarer Algorithmus.

Post by Ingo Menger
Ja schon, nur ist es eben absolut trivial, einen solchen Ablauf als
Nachbedingung umzuformulieren, indem ich für einen Ausdruck x, der den
"Ablauf" beschreibt immer
result == x schreibe. Siehe oben.

Ja, aber Spezifikation funktioniert ja nun nicht so, dass ich den
Algorithmus angebe. Dessen Korrektheit will ich ja gerade überprüfen
bzw. Fehler bei der Umsetzung erkennen. Wenn ich Mergesort als
Nachbedingung angebe, kann ich ihn auch gleich implementieren.

[Stefan Ram]

Post by Daniel Thoma
Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: (\forall A'_i, A'_j, i < j; A'_i < A'_j) && (\forall A_i
\e𝄪ists j: A_i = A'_j && |A| = |A'|)

array(A) ∧
array(A') ∧
range(A)=range(A') ∧
domain(A)=domain(A') ∧
|A| = |A'| ∧
∀a ∈ range(A):(|{ i | A(i) = a }| = |{ i | A'(i) = a }|) ∧
∀i,j ∈ domain(A'):(i ≤ j ⇒ A'(i) ≤ A'(j))

[Stefan Ram]

[Supersedes zur Korrektur fehlerhafter Zeichen]

Post by Daniel Thoma
Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: (\forall A'_i, A'_j, i < j; A'_i < A'_j) && (\forall A_i
\exists j: A_i = A'_j && |A| = |A'|)

array(A) ∧
array(A') ∧
range(A)=range(A') ∧
domain(A)=domain(A') ∧
|A| = |A'| ∧
∀a ∈ range(A):(|{ i | A(i) = a }| = |{ i | A'(i) = a }|) ∧
∀i,j ∈ domain(A'):(i ≤ j ⇒ A'(i) ≤ A'(j))

[Ingo Menger]

Post by Daniel Thoma

Post by Ingo Menger
Nein, das ist völlig unterspezifiziert.

Das einzige, was fehlt, ist, dass hinterher die gleichen Elemente im
Vorbedingung: \forall A_i, A_j, i != j: A_i != A_j
Nachbedingung: (\forall A'_i, A'_j, i < j; A'_i < A'_j) && (\forall A_i
\exists j: A_i = A'_j && |A| = |A'|)
Der ' bedeutet, dass es sich um den Zustand nach der Ausführung handelt.
Damit ist also ausgedrückt, dass man ein Array will, das gleich lang
ist, das alle Elemente enthält und das sortiert ist.

Das reicht leider noch immer nicht für die Praxis, da sollte noch
Stabilität drin sein.

Post by Daniel Thoma

Post by Ingo Menger
Nein. Da müßtest Du schon genauer spezifizieren.
sort A
pre: /* A is an array */
post: result == merge (sort erste-hälfte) (sort zweite_hälfte)
where erste_hälfte = // konstruiere eine Hälfte
zweite_hälfte = // konstruiere andere Häkfte
merge A B = // mische zwei sortieite Arrays

Das ist keine Spezifikation, das ist ein Algorithmus.

Nein und Ja.

Post by Daniel Thoma
Nachbedingung ist hier also, das Ergebnis soll das Ergebnis von
Mergesort sein.

Besser: es soll mergesorted sein, d.h. die gleichen Eigenschaften
haben, wie wenn ich das Ausgangsarray mit Mergesort behandelt hätte.
Zufällig ist der offensichtlichste Weg, dies zu erreichen,
tatsächlich Mergesort zu implizieren.

Post by Daniel Thoma
Es genügt aber einfach anzugeben, wie man überprüft,
dass ein Array sortiert ist. (Das ist, was ich gemacht habe.)

Es würde genügen, wenn Du die Stabilitätsbedingung mit reinnimmst.
Aber Deine Sprache ist nicht so gut geeignet, einen Algorithmus
abzuleiten.

Post by Daniel Thoma
Das
Beispiel Sortierung habe ich natürlich gewählt, weil es sehr einfach
ist, zu prüfen, dass ein Array sortiert ist.

Das scheint nur so. Es fehlt ja noch die Stabilitätsbedingung. Und die
ist gar nicht so trivial.

Post by Daniel Thoma

Post by Ingo Menger
Ja schon, nur ist es eben absolut trivial, einen solchen Ablauf als
Nachbedingung umzuformulieren, indem ich für einen Ausdruck x, der den
"Ablauf" beschreibt immer
result == x schreibe. Siehe oben.

Ja, aber Spezifikation funktioniert ja nun nicht so, dass ich den
Algorithmus angebe.

Derzeit nicht.

Post by Daniel Thoma
Dessen Korrektheit will ich ja gerade überprüfen
bzw. Fehler bei der Umsetzung erkennen. Wenn ich Mergesort als
Nachbedingung angebe, kann ich ihn auch gleich implementieren.

Ja, warum nicht, wenn die verwendete Sprache "abstrakt genug" ist.
Wobei letzteres natürlich ein "weiches" Kriterium ist.

[Daniel Thoma]

Post by Ingo Menger
Das reicht leider noch immer nicht für die Praxis, da sollte noch
Stabilität drin sein.

Verwendest Du nie Quicksort? Stabilität ist sicher eine interessante
Eigenschaft, aber man muss die weder immer haben, noch hat man sie in
der Praxis immer. Bei den Sortiermethoden in der Collections-API von
Java wird das überall gefordert und implementiert ok.
Ich habe mich ja auf Arrays ohne mehrfache Elemente beschränkt, setzen
wir also erst einmal Stefans Definition voraus, die auch mit mehrfachen
Elementen klar kommt.
Um Stabilität zu spezifizieren, muss irgendwie die Identität von
Elementen festgestellt werden können. Es muss also eine
Äquivalenzrelation geben, die "stärker" als die (partielle)
Ordnungsrelation ist, d.h. es muss gelten: a == b --> (a <= b \and b >=
a) aber im Allgemeinen nicht umgekehrt.
Dafür können wir einfach == aus Java nehmen.
Nun müssen wir die Stabilität spezifizieren, also dass sich die
Reihenfolge von Elementen, die bezüglich der Ordnungsrelation gleich
sind, nicht ändert:

\forall i,j, i < j: ((A[i] <= A[j] \and A[j] <= A[i]) --> (\exists i',
j', i' < j': A[i] == A'[i'] \and A[j] == A'[j']))

So schwierig war es doch gar nicht?

Post by Ingo Menger

Post by Daniel Thoma
Das ist keine Spezifikation, das ist ein Algorithmus.

Nein und Ja.

Post by Daniel Thoma
Nachbedingung ist hier also, das Ergebnis soll das Ergebnis von
Mergesort sein.

Toll, dann ist aber nicht die Spezifikation das Programm sondern das
Programm die Spezifikation. Man will ja gerade Implementierungsfehler
vermeiden und gibt deswegen eine Spezifikation an, die einfacher sein
soll. Formale Spezifikationen sind nun idR. sowieso nicht einfach und
ich glaube daher auch nicht, dass vollständige formale Spezifikation je
in der Breite angewendet werden wird. Wenn man dann aber noch das
Programm direkt daraus erzeugt, bzw. statt zu spezifizieren gleich in
einer noch etwas abstrakteren Sprache das Programm aufschreibt, dann
erreicht man nicht mehr die Sicherheit, die man eigentlich haben wollte.
Es werden ja nicht mehr zwei Beschreibungen gegeneinander geprüft und
die Beschreibung ist noch nicht mal einfacher, als die Implementierung.

Post by Ingo Menger
Es würde genügen, wenn Du die Stabilitätsbedingung mit reinnimmst.
Aber Deine Sprache ist nicht so gut geeignet, einen Algorithmus
abzuleiten.

Meine Sprache ist eben eine Spezifikationssprache klar. Das hat aber
noch nicht mal direkt mit der Sprache zu tun. Die Überprüfung kann man
ja sogar direkt in einer Programmiersprache hinschreiben.
Der Unterschied ist also nicht die Sprache, sondern dass ich Bedingungen
angegeben habe, aus denen es nicht einfach ist, einen Algorithmus zu
bestimmen. Und das gilt eben praktisch immer, wenn man nicht den
Algorithmus selbst als Spezifikation verwendet.

Post by Ingo Menger
Das scheint nur so. Es fehlt ja noch die Stabilitätsbedingung. Und die
ist gar nicht so trivial.

Sie lässt sich mit der entsprechenden Sprache schon noch recht einfach
beschreiben. Die Überprüfung ist natürlich nicht mehr so einfach, wie
bei der Sortierung. Das bedeutet aber nur, dass sich solche Bedingungen
noch nicht mal für Laufzeitzusicherungen wirklich eignen. Für eine
Spezifikations ist das aber erstmal kein Problem.

Post by Ingo Menger
Derzeit nicht.

Naja man kann das auch derzeit machen. Nimm halt eine Programmiersprache
und schreib deine Spezifikation damit. Als Programmgenerator kann man
die Identitätsfunktion verwenden ;)

Post by Ingo Menger
Ja, warum nicht, wenn die verwendete Sprache "abstrakt genug" ist.
Wobei letzteres natürlich ein "weiches" Kriterium ist.

Was Du willst, sind wohl einfach Programmiersprachen, die abstrakter
sind. Also irgendetwas funktionales oder logisches, das ein bisschen
weiterentwickelt ist.
Weiterentwicklung von Programmiersprachen ist auch wichtig,
Spezifikation mit Vor- und Nachbedingungen, Invarianten usw. wie das OCL
erlaubt, ist eben was anderes.

[Wanja Gayk]

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Das mit dem niemals würde ich so nicht stehen lassen... Die Ewigkeit ist
eine solch lange Zeit.

Aber hier kann das 'niemals' mit Sicherheit stehen bleiben. ;-)
Das hat die theoretische Informatik i.A. bewiesen...

Wie schön dass zwar nicht jedes mögliche Programm verifiziert werden
kann (Halteproblem), aber dennoch eine Teilmenge. Und weil es unendlich
viele Programme geben kann, gibt es auch unendlich viele beweisbare
Programme. Stellt sich nur die Frage, in wie fern sich die Analyse von
Programmteilen vom Zeitaufwand her lohnt.

Eine IDE, die zumindest die Programmteile kennzeichnet, von denen die
Korrektheit/Unkorrektheit bewiesen werden kann, wäre schon nicht übel.
Bisher beschränkt sich das ja nur auf die Kennzeichnung der
Unkorrektheit einfacher Nullchecks, wenige boolesche Ausdrücke und
überflüssige instanceof-Operatoren und das noch nicht mal über
Methodengrenzen hinweg.

Gruß,
-Wanja-

[Jochen Theodorou]

Post by Gerd K.

Post by Jochen Theodorou

Post by Gerd K.
Unabhängig von der Semantikfrage: Es wird niemals einen
automatischen Programmverifizierer geben können.
Deswegen werden wir immer weiter Testen müssen.. ;-)

Das mit dem niemals würde ich so nicht stehen lassen... Die Ewigkeit ist
eine solch lange Zeit.

Aber hier kann das 'niemals' mit Sicherheit stehen bleiben. ;-)
Das hat die theoretische Informatik i.A. bewiesen...

Jeder Beweis geht von bestimmten Axiomen aus. Axiome sind es ja deshalb,
weil es nicht beweisbare Aussagen sind. Stellt man nun fest, das ein
Axiom nicht richtig ist, dann sind alle Beweise, die darauf aufbauen
eventuell falsch.

Sollte es sich also herausstellen das ein Axiom falsch ist, kann das
extreme Auswirkungen in einer ansonsten korrekten Aussage haben. Und es
gibt einen Haufen Axiome.

Gruss theo

[Stefan Ram]

Post by Jochen Theodorou
Sollte es sich also herausstellen das ein Axiom falsch ist,

Es gibt keine "falschen Axiome", höchstens "inkonsistente
Axiomsysteme".

[Jochen Theodorou]

Post by Stefan Ram

Post by Jochen Theodorou
Sollte es sich also herausstellen das ein Axiom falsch ist,

Es gibt keine "falschen Axiome", höchstens "inkonsistente
Axiomsysteme".

Wenn ich ein System basierend aus Axiomen habe und 2 Axiome schliessen
sich gegenseitig aus, das System ist aber mit jeweils einem Axiome
vollständig... dann bin ich angeschmiert, oder?

[Stefan Ram]

Post by Jochen Theodorou

Post by Stefan Ram
Es gibt keine "falschen Axiome", höchstens "inkonsistente
Axiomsysteme".

Wenn ich ein System basierend aus Axiomen habe und 2 Axiome
schliessen sich gegenseitig aus, das System ist aber mit
jeweils einem Axiome vollständig... dann bin ich angeschmiert,
oder?

Axiomensysteme werden so aufgestellt, daß sie für ein
bestimmtes Ziel dienlich sind oder mit einer zunächst intuitiv
entstandene Theorie verträglich sind. Ein Axiomsystem darf
dabei auch aus nur einem einzigen Axiom bestehen. Wenn das
einzige Axiom eine Elementaraussage ist, dann kann es nicht
inkonsistent zu sich selbst sein.

[Jochen Theodorou]

Post by Stefan Ram

Post by Jochen Theodorou

Post by Stefan Ram
Es gibt keine "falschen Axiome", höchstens "inkonsistente
Axiomsysteme".

Wenn ich ein System basierend aus Axiomen habe und 2 Axiome
schliessen sich gegenseitig aus, das System ist aber mit
jeweils einem Axiome vollständig... dann bin ich angeschmiert,
oder?

Axiomensysteme werden so aufgestellt, daß sie für ein
bestimmtes Ziel dienlich sind oder mit einer zunächst intuitiv
entstandene Theorie verträglich sind. Ein Axiomsystem darf
dabei auch aus nur einem einzigen Axiom bestehen. Wenn das
einzige Axiom eine Elementaraussage ist, dann kann es nicht
inkonsistent zu sich selbst sein.

Klar, aber in der Regel ist es mehr als ein Axiom. Manchmal stecken die
Axiome auch im BEweissystem selber und sind garnicht explizit als Axiom
zu erkennen.

Gruss theo

[Niko Schwarz]

On Thu, 14 Sep 2006 15:59:01 +0200, Jochen Theodorou

Post by Jochen Theodorou
Wenn ich ein System basierend aus Axiomen habe und 2 Axiome schliessen
sich gegenseitig aus, das System ist aber mit jeweils einem Axiome
vollständig... dann bin ich angeschmiert, oder?

Allerdings. Ein widersprüchliches Axiomsystem hat nämlich nur genau
einen Wahrheitswert, was hinderlich ist, wenn man falsche von wahren
Aussagen unterscheiden möchte.

(Ein Widerspruch liegt vor, falls eine Aussage sowohl wahr als auch
falsch ist, Sei Aussage A diese, W der Wahrheitswert "wahr", F der
Wahrheitswert "falsch": A <=> W AND A <=> F. Weiterhin gilt für
beliebige Aussagen B, C,D: Aus B <=> C und C <=> D folgt B <=> D
[Transitivität]. Insgesamt erhält man W <=> F, das heißt wahr und
falsch bedeuten dasselbe und DAS heißt, man ist angeschmiert.)

slt,

niko

[Jochen Theodorou]

Post by Niko Schwarz
On Thu, 14 Sep 2006 15:59:01 +0200, Jochen Theodorou

Post by Jochen Theodorou
Wenn ich ein System basierend aus Axiomen habe und 2 Axiome schliessen
sich gegenseitig aus, das System ist aber mit jeweils einem Axiome
vollständig... dann bin ich angeschmiert, oder?

Allerdings. Ein widersprüchliches Axiomsystem hat nämlich nur genau
einen Wahrheitswert, was hinderlich ist, wenn man falsche von wahren
Aussagen unterscheiden möchte.

Du Mißverstehst... Ich sagte das System ist vollständig wenn nur eines
der Axiome besteht und das andere ignoriert wird. Es ergeben sich also
effektiv 2 Systeme, mit Aussagen, die in beiden richtig sind und
Aussagen, die in einem richtig, in dem anderen aber falsch sind. Ich
kann kein Axiomensystem benutzen das sich wiedersprechende Axiome enthält

Gruss theo

[Frank Stolle]

Hallo Frank,

Post by frankmusolf
habe neulich entdeckt, dass findbugs die möglichkeit bietet, mit
annotations quasi design by contract bedingungen zu formulieren.

vielen Dank für den Hinweis. Finde ich ein sehr nützliches Tool und
werde es einmal richtig austesten.

Grüße

Frank

[frankmusolf]

hier noch ein ganz guter text über ESCJava und findbugs:
https://projects.mi.fu-berlin.de/w/pub/SE/SeminarFehlerSoftwareentwicklung2004/paper16c.pdf#search=%22escjava%22