Verifikation einer if-Bedingung

N

neuer Nutzer

Gast
Ich habe ein Problem mit einer Aufgabe bzw. Beweis über die Verifikation zu einer if Anweisung.

Folgender Programmtext ist gegeben:
Java:
if (a > 0) {
a = a + 2 * b;
c = a / 2 + 1;
} else {
a = -a;
a = 3 * a + b;
c = a + 1;
}

Gegeben ist noch die Vorbedingung: b>0 sowie die Nachbedingung c>=2.

Wir haben folgende Beweismethode gewählt. Und zwar sollen wir von der Nachbedingung zur Vorbedingung folgern.

Das würde also so aussehen:

Java:
{b>0}//Vorbedingung

if (a > 0) {
	a = a + 2 * b;
	c = a / 2 + 1;
}else{
	a = -a;
	a = 3 * a + b;
	c = a + 1;
}

{c>=2}//Nachbedingung

Um zu zeigen, dass die Vorbedinung if B {alpha} else {beta} Nachbedingung gilt, soll man zeigen:
{Vorbedingung und B} alpha {Nachbedingung} sowie{Vorbedingung und B negiert} beta {Nachbedingung}.

Das habe ich angewendet:
Java:
{b>0}

if (a > 0) {
	{b>0 und a>0}
	a = a + 2 * b;
	{a/2 +1>=2} 
	c = a / 2 + 1;
	{c>=2}
}else{
	{b>0 und a <= 0}
	a = -a;
	a = 3 * a + b;
	{a+1>=2}
	c = a + 1;
	{c>=2}
}

{c>=2}
Betrachten wir einmal nur den else-Zweig. Vielleicht genügt mir das schon, um es zu verstehen. Ich weiß also, dass die Nachbedingung c>=2 lautet. Das bedeutet, dass a+1>=2 gelten muss. Also umgeformt: a>=1. Jetzt komme ich dann zu dem Text: "a=3*a+b". Wie kann ich nun weiter folgern? Wäre dies hier korrekt: Ich weiß nun, dass a>=1 gilt. Also muss 3*a+b>=1 sein. Nur wie kommt man nun auf die Vorbedingung, dass b>0 sein soll und a<=0?
 
Zuletzt bearbeitet von einem Moderator:
S

SlaterB

Gast
> Und zwar sollen wir von der Nachbedingung zur Vorbedingung folgern.

gewagt gewagt, sehe ich nicht so und bereitet dir hier auch unnötige Schwierigkeiten,
da du sowieso schon soviel hast kann ich mal in ganzen Lösungen antworten:

folgere aus den Vorbedingungen die Nachbedingung! das ist doch der viel klarere Weg, das ist doch der Sinn dieser Begriffe!

Java:
{b>0 und a <= 0} // hier gehts los, unten ist das Ende!
a = -a;
{b>0 und a >= 0} // a umgedreht
a = 3 * a + b;
{a>=1} // a ist vielleicht 0, aber b ist ja mindestens drin, Summe ist mindestens 1
c = a + 1;
{c>=2} // trivial, das vorherige und noch 1 drauf

edit:
"von der Nachbedingung zur Vorbedingung folgern"
führt bei google nur zu diesem Thema hier als einzige Link ;),
aber das muss natürlich nichts heißen
"von der Vorbedingung zur Nachbedingung folgern" findet gar keien direkten Ergebnisse,
dieses Thema hier im weiteren schon wieder der dritte Link,

jedes Mal erstaunlich wie stark und schnell gerankt
(hoffentlich nicht nur weil google weiß dass ich eh grad hier war,
gar von meiner geheim geloggten Historie überhaupt erst die Seite aufgenommen ;) )

edit:
"von der Vorbedingung zur Nachbedingung"
führt dann aber zu einen PDF in welchem der Rückweg auch genannt wird, also ok
 
Zuletzt bearbeitet von einem Moderator:
N

Neuer Nutzer

Gast
Danke für deine Antwort. Von der Vorbedingung zur Nachbedingung zu folgern ist in diesem Fall doch um einiges einfacher.

Noch eine Frage:

Was bedeutet die Vorbedingung true denn? Wie verwerte ich das nach dem von dir beschriebenen Schema?
 
S

SlaterB

Gast
dazu fällt mir nichts ein, was ich mit Überzeugung als sinnvolle/ bekannte Antwort bezeichen könnten
(ob richtig oder falsch ist eh immer offen)

einfach so überlegt wäre "true" für mich überhaupt nichts als Vorbedingung,
{b>0}
könnte man auch als
{b>0 AND true}
oder
{b>0 AND true AND true AND true AND true AND true}
schreiben, was macht das schon..

fällt b>0 weg, bleibt eben nur true übrig

-----

dazu gilt ja noch der Merksatz, dass man im Gegensatz aus false alles folgern kann (jedenfalls ist die Implikation logisch korrekt),
also würde 'aus true kann man nichts folgern' zunächst gut klingen
 
Zuletzt bearbeitet von einem Moderator:
N

Neuer Nutzer

Gast
Ein Beispiel aus unserer Vorlesung:

{true}
if(a<3){
{true und a<3}
c=b+3;
{c>=b+3}
}else{
{true und a>=3}
c=a+b;
{c>=b+3}
}
{c>=b+3}

in geschweiften Klammern stehen immer die Vor und Nachbedingungen.

Die Folgerung sieht dann so aus:
{true}
if(a<3){
{true und a<3}
{b+3>=b+3}
c=b+3;
{c>=b+3}
}else{
{true und a>=3}
{a+b>=b+3}
c=a+b;
{c>=b+3}
}
{c>=b+3}

Hier wurde wieder "von unten nach oben" bewiesen.

Es macht schon Sinn, was nun dort steht. {a+b>=b+3} umgeformt bedeutet, {a>=3} Also die Vorbedingung und das true kann man ja, wie du schon angemerkt hast, beliebig oft anfügen.
Im if-Zweig steht b+3>=b+3. Das ist true. Aber wie kommt man auf a<3?
 

Final_Striker

Top Contributor
Benutze bitte Java Tags, wie es dick und rot über dem Eingabefenster steht. Dabei bleibt das Format erhalten, sonst kann das doch kein Mensch richtig lesen!

Java™ Quelltext ist bitte in [ JAVA]-Tags zu schreiben: [ JAVA]hier Java Code einfügen[/ JAVA]
 
N

Neuer Nutzer

Gast
Hierzu habe ich noch eine Frage:
Vorbedingung: true und a>0 und b<=0.
Java:
else {
{true und a>0 und b<=0}
c = a * b * (-1);
{c>=2}
}
Nachbedingung: c>=2.

Wie kommt man nun darauf? Wenn ich von oben nach unten beweisen möchte, dann ist ja b unter Umständen Null. Positiv (oder 0) ist es auf jeden Fall, da a >0 ist. Aber warum muss c>=2 sein?
 
S

SlaterB

Gast
true steht also für die Art nichts, aus der man etwas folgern/ hinzufügen kann wenn es sich aus dem folgenden Code von selbst ergibt,
ohne Vorbedingung, das ist wiederum sinnvoll

'Wie kommt man nun darauf?' bei Zweifel der Richtigkeit muss man gar nicht fragen,
denn Widerlegen ist zum Glück immer einfacher als Beweisen, Wiederlegungsbeweis durch Beispiel,
0 muss nicht mal vorkommen, reicht auch a = 1 und b = -1, dann ist c = 1, Ende mit der Nachbedingung,

daraus folgt dass entweder
a) die Nachbedingung falsch ist, warum auch immer, oder
b) nicht alle Rahmenbedingungen der Aufgabe korrekt verstanden sind, was vielleicht deine Frage ist, durchaus berechtigt, aber mir geht es da nicht anders,

in beiden Fällen muss man jedenfalls nicht über den Beweis nachdenken ;)
entweder gibts keinen oder man muss schon viel grundsätzlicher nachdenken

------

> Aber wie kommt man auf a<3?
na jedenfalls nicht durch die nachfolgenden Zeilen, das kommt vom if/else,
inwiefern 'rückwärts' hier Sinn zustande kommt mag ich (auch) nicht nachvollziehen,
vielleicht kann man irgendwann auch mit 'rückwärts' aufhören und zum Teil wenigstens auch vorwärts gehen
 
Zuletzt bearbeitet von einem Moderator:
N

Neuer Nutzer

Gast
Na ja, hier noch einmal die komplette Aufgabe:

Verifizieren Sie den folgenden Programmabschnitt bezüglich der Vorbedingung true und
Nachbedingung c ≥ 0. Fügen Sie dabei Bedingungen (ca. 15) und Begründungen in den Pro-
grammtext ein, so dass alle Beweisschritte leicht nachvollzogen werden können.

Java:
if (a > 0) {
if (b > 0) {
c = a * b;
} else {
c = a * b * (-1);
}
} else {
a = -a;
if (b < 0) {
b = -b;
}
c = a * b;
}

Wenn ich nach dem Beweisschema, welches wir in der Vorlesung besprochen haben und ich hier auch schon erklärt habe, vorgehe, gelange ich zu folgendem im vorherigen Post beschriebenen Programmtext. Daraus kann man ja dann folgern, dass das Programm nicht korrekt läuft?

Ein bisschen unsicher macht mich aber die Aufgabenstellung. Unter der Aufforderung "verifizieren SIe..." würde ich jetzt noch nicht ableiten, dass das Programm korrekt ist. Aber wenn man 15 Bedingungen angeben soll, macht mich das ein bisschen skeptisch.
 
S

SlaterB

Gast
die Nachbedingung ist nun nur noch "c ≥ 0",
das ist nach Adam Riesling und Eva Textvergleich was anderes als zuvor "c>=2"

mit soviel Verzweigungen darfst du sicher ca. 15 Kleinigkeiten einfügen, viel Spass!
 
Ähnliche Java Themen
  Titel Forum Antworten Datum
K Hoar-Kalkül,verifikation&schleifeninvariante? Java Basics - Anfänger-Themen 4
M Ausgabe einer ArrayList ensteht nur als Hashcode, nicht als Objekt Java Basics - Anfänger-Themen 16
D 2 ArrayListen gleich sortieren bzw. eine Liste anhand einer anderen Sortieren Java Basics - Anfänger-Themen 6
ixChronos Letzten 4 Ziffern einer großen Zahl ausgeben Java Basics - Anfänger-Themen 3
P Objekt einer Methode eines anderen Objektes übergeben Java Basics - Anfänger-Themen 5
L Variablenwerte aus einer Methode übergeben Java Basics - Anfänger-Themen 2
E Arrays in einer ArrayList miteinander vergleichen Java Basics - Anfänger-Themen 12
Simon16 Java ArrayListe von einer Klasse sortieren Java Basics - Anfänger-Themen 2
Shadowrunner Variablen Gibt es eine Möglichkeit die Ziffern/Stellen einer Zahl fest zu legen? Java Basics - Anfänger-Themen 3
D remove Object von einer Liste von Obejcts Java Basics - Anfänger-Themen 3
FunkyPhil94 Wert in einer Lambda Funktion erhöhen Java Basics - Anfänger-Themen 3
T Aufruf der Methode einer Oberklasse, wenn sie in der Unterklasse überschrieben ist. Polymorphie. Java Basics - Anfänger-Themen 2
B Kommunikation mit Seriellen Schnittstellen + Integration einer lib Java Basics - Anfänger-Themen 1
A Daten aus einer HashMap aus einer DB speichern und mit neuen Werten vergleichen Java Basics - Anfänger-Themen 8
P Welches SDK für das erstellen einer ausführbaren Datei? Java Basics - Anfänger-Themen 4
D Länge einer Liste aufrufen. Java Basics - Anfänger-Themen 19
J Klassen Instanzen einer Klasse in einer anderen unabhängigen Klasse nutzen Java Basics - Anfänger-Themen 4
B Alle Strings bis zu einer Maimallänge aufzählen, die Bedingung erfüllen Java Basics - Anfänger-Themen 13
marcelnedza Finde meinen Fehler in einer Methode nicht, Java Karol Java Basics - Anfänger-Themen 15
Soranix Erste Schritte Struktur als Anfänger // Von einer Klasse auf ein Objekt einer anderen Klasse zugreifen. Java Basics - Anfänger-Themen 6
MoxMorris Wie macht man String[] = String[] aus einer anderer Methode? Java Basics - Anfänger-Themen 18
T Fibonacci mit einer Hilfsmethode berechnen Java Basics - Anfänger-Themen 10
S Hilfe zu einer Aufgabe Java Basics - Anfänger-Themen 5
M Radius von einer ellipse bestimmen Java Basics - Anfänger-Themen 7
Say Fehlenden Code finden in einer while-Schleife? Java Basics - Anfänger-Themen 11
M Zufallszahl generieren mit einer linken und rechten Grenze Java Basics - Anfänger-Themen 3
N Was Passiert mit dem Namen einer Variable, wenn man diese einer Liste Hinzufügt Java Basics - Anfänger-Themen 16
_user_q Wie eine Methode/Funktion aus einer Klasse mit Constructor aufrufen? Java Basics - Anfänger-Themen 20
W String einer Textdatei in einzelne Stringobjekte pro Zeile aufteilen Java Basics - Anfänger-Themen 14
W Objekte einer ArrayList in txt-datei schreiben mit Paths? Java Basics - Anfänger-Themen 2
S Best Practice Fragen zu Projektstruktur einer Datenbank-Abfrage-App (MVC) Java Basics - Anfänger-Themen 13
T Variable von Objekten in einer Methode überprüfen Java Basics - Anfänger-Themen 26
nelsonmandela Problem bei Ausgabe einer Switch - Case Funktion Java Basics - Anfänger-Themen 5
S Textausgabe in einer For-Schleife Java Basics - Anfänger-Themen 12
M Spezifischen Wert einer Zeile aus .txt Datei entnehmen Java Basics - Anfänger-Themen 15
B Popups mit Klicksabfangen zumAusfüllen einer .ods Datei Java Basics - Anfänger-Themen 0
M RandomAccessFile int und String gleichzeitig in einer Datei Java Basics - Anfänger-Themen 49
E Suchfunktion in einer Liste Java Basics - Anfänger-Themen 39
T ungeordnete Werte-Paare in einer Liste Java Basics - Anfänger-Themen 7
FireHorses Einen Command erst nach einer Chateingabe aktivieren Java Basics - Anfänger-Themen 1
frager2345 Singleton-Muster Java ->Nur eine Instanz einer Klasse erzeugen können Java Basics - Anfänger-Themen 45
F wie kann ich die Position des letzten Vokals innerhalb einer Zeichenkette ermitteln? Java Basics - Anfänger-Themen 5
H Kapselung protected aber in einer Kindklasse nicht zugänglich Java Basics - Anfänger-Themen 5
R Methoden Werte einer ArrayList als Parameter übergeben. Java Basics - Anfänger-Themen 4
B Den Dateipfad einer Java Datei durch Code in Selbiger finden? Java Basics - Anfänger-Themen 10
LilliCherry Array in einer Zeile ausgeben Java Basics - Anfänger-Themen 6
B Attribute eines Objekts einer Klasse durch statische Methode einer 2. Klasse ändern? Java Basics - Anfänger-Themen 32
L Dauerhaftes Speichern einer Eingabe bei einer ArrayList Java Basics - Anfänger-Themen 26
V Hilfe bei Implementierung einer boolean Methode Java Basics - Anfänger-Themen 6
G Position einer unbekannten 3-stelligen-Zahl in einem String finden Java Basics - Anfänger-Themen 15
stormyark Fehler beim überschreiben einer Variable Java Basics - Anfänger-Themen 1
H Kompliziertes Sortieren einer ArrayList mit Objekten(Sortieren nach X und Y) Java Basics - Anfänger-Themen 11
T Permanentes speichern von Objekten in einer ArrayList Java Basics - Anfänger-Themen 6
Saiko Zeilen einer Datei einlesen Java Basics - Anfänger-Themen 3
H Erste Schritte Nach einer Zahl n soll n Mal der String untereinander ausgegeben werden Java Basics - Anfänger-Themen 3
G zwei Instanzen einer Klasse Java Basics - Anfänger-Themen 29
sserio Prüfziffer einer ISBN Nummer herrausfinden. Java Basics - Anfänger-Themen 14
J Benennung einer mir unbekannten Java - Ausdrucksweise Java Basics - Anfänger-Themen 5
LFB In einer For-Schleife alles in einer Zeile ausgeben Java Basics - Anfänger-Themen 14
sserio Wie kann man nach einer Klasse fragen? Java Basics - Anfänger-Themen 12
berserkerdq2 Wann soll ich den Stream schließen, wenn ich das in einer Methode habe? Java Basics - Anfänger-Themen 8
berserkerdq2 Wie gebe ich den Pfad zu einer Datei an, die in einem Ordner in Eclipse ist? Java Basics - Anfänger-Themen 1
M Variable in einer Schleife initialisieren Java Basics - Anfänger-Themen 46
D EinMalEins mithilfe einer for-Schleife und Array Java Basics - Anfänger-Themen 1
J int innerhalb einer Datei ändern Java Basics - Anfänger-Themen 1
D Hilfe bei einer Aufgabe mit for-Schleife Java Basics - Anfänger-Themen 6
Neuling47 Ich zerbreche mit den kopf an einer Aufgabe Java Basics - Anfänger-Themen 61
H Mit setter-Methode JLabel in einer andern Klasse ändern. Java Basics - Anfänger-Themen 40
J Zelleninhalt einer Jtable löschen Java Basics - Anfänger-Themen 2
Robert_Klaus Hamster java Simulation Hilfe bei einer Aufgabe Java Basics - Anfänger-Themen 5
stormyark 4 Bit in einer for-schleife funktioniert nicht Java Basics - Anfänger-Themen 3
F Werte in einer Arraylist Zählen Java Basics - Anfänger-Themen 2
M ArrayList mit einer Schleife befüllen Java Basics - Anfänger-Themen 2
A Ein Array bearbeiten und in einer anderen Methode nutzen Java Basics - Anfänger-Themen 6
A Ergebnis einer Methode bei einer anderen verwenden Java Basics - Anfänger-Themen 13
I Interface von einer EJB Klasse, um Code zu reduzieren Java Basics - Anfänger-Themen 1
M Interface als Parameter einer Klasse Java Basics - Anfänger-Themen 8
I Liste von Infos von einer eigenen Annotation in Liste speichern Java Basics - Anfänger-Themen 0
M Wie kann ich den Index i von einer LinkedList überprüfen? Java Basics - Anfänger-Themen 36
M Wie kann die Implementation einer Methode den Wert eines Attributs vermindern? Java Basics - Anfänger-Themen 3
M Wie verknüpfe ich eine Bedingung mit einer Methode ohne if-Verzweigung & Bedingungsoperator? Java Basics - Anfänger-Themen 2
P Doppelte werte in einer Liste zählen Java Basics - Anfänger-Themen 11
javapingu Jeglichen Inhalt einer Textdatei nach Zeile n löschen Java Basics - Anfänger-Themen 8
D mehrere Berechnungen in einer Methode Java Basics - Anfänger-Themen 9
P Iterieren mit einer Foreach in Lambdaschreibweise und Counter. Java Basics - Anfänger-Themen 1
M Methoden Wert einer Variable geht verloren? Java Basics - Anfänger-Themen 6
W Wie ziehe ich von einer bestimmten Zahl, Zahlen ab, bis mein Ergebnis null beträgt? Java Basics - Anfänger-Themen 10
X Was ist der Unterschied zwischen materialisierten und nichtmaterialisierten Attributen einer Klasse? Java Basics - Anfänger-Themen 1
U Wie ein Attribut von einer Klassenmethode in der Klasse speichern= Java Basics - Anfänger-Themen 2
M Wie richte ich eine Diagonale an Robotern in einer World ein? Java Basics - Anfänger-Themen 15
YAZZ BlueJ Bewegung einer Figur im Kreis Java Basics - Anfänger-Themen 4
O Ich habe einen String und soll mit matches schauen, ob ein Buchstabe zu einer geraden ANzahl im String vorkommt, wie soll das gehen? Java Basics - Anfänger-Themen 7
A Verarbeiten einer Excel Datei durch das java-Programm Java Basics - Anfänger-Themen 3
B GUI extension mit einer Liste verbinden Java Basics - Anfänger-Themen 1
O Wie erstelle ich eine Instanz in einer Klasse für die ich die Instanz will? Java Basics - Anfänger-Themen 4
S Hilfe bei Programmierung einer Hotelabrechnung Java Basics - Anfänger-Themen 5
W Verschiedene Methoden in einer Klasse in der Main aufrufen? Java Basics - Anfänger-Themen 8
J if-Schleife innerhalb einer if-Schleife wird in der Konsole nicht gelesen Java Basics - Anfänger-Themen 4
D Grösste Zahl in einer Folge herausfinden. (ULAM) Java Basics - Anfänger-Themen 9
Ameise04 Variablen Inhalt einer Variable im Code verwenden? Java Basics - Anfänger-Themen 9

Ähnliche Java Themen

Neue Themen


Oben