[ALG] Wat is een invariant?

Pagina: 1
Acties:
  • 308 views sinds 30-01-2008
  • Reageer

Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Op dit moment ben ik in de avond uren bezig me AMBI HP1 (software engineering). Het belangerijkste onderdeel is het ontwerpen van algoritmen.

In het boek wordt uit gelegd wat een invariant is (pascal notatie, wordt ook in het boek gebruikt):
{P} //preconditie
while B do
begin
{P && B}
S //opdracht
{P}
end
{P && !B}
{Q} //postconditie

Als B waar is dan wordt de while lus gestart, dus dan geldt: {P && B}. Als geldt {P && !B} dan wordt de lus verlaten. Uit {P && !B} volgt Q de postconditie. Tot zover kan ik het allemaal nog goed volgen.

Volgens het boek is een invariant, een uitspraak P met de eigenschap {P && B} S {P}. Dit zegt me eigenlijk niet zoveel, wie kan me in gewoon nederlands uitleggen wat een invariant is en waarvoor een invariant dient?

Zijn er trouwens nog meer mensen hier op Tweakers die AMBI, de HP richting doen?

Acties:
  • 0 Henk 'm!

  • Alarmnummer
  • Registratie: Juli 2001
  • Laatst online: 09-07-2024

Alarmnummer

-= Tja =-

Ik neem aan dat je weet wat design by contract is?

Een invariant is iets dat altijd geld.
Bv... als ik geld overmaak van jouw rekening, naar mijn rekening... dan moet voor en na deze actie gelden: het totaal aan geld is gelijk.

Een preconditie = iets dat moet gelden als je ergens aan begint..

Een postconditie = iets dat moet gelden als je er mee klaar bent.

Acties:
  • 0 Henk 'm!

  • Robtimus
  • Registratie: November 2002
  • Laatst online: 19:39

Robtimus

me Robtimus no like you

Wat Alarmnummer zegt: een invariant is iets dat aan het begin en einde van elke loop (en in meer ingewikkelde contexten zelfs gedurende hele programma's) moet gelden; het is ook INvariant (als in niet-variant).

En waar het voor geldt? Simpel: met invarianten kun je bewijzen dat programma's correct zijn. Heb er zat mee te maken gehad op de TU/e.

More than meets the eye
There is no I in TEAM... but there is ME
system specs


Acties:
  • 0 Henk 'm!

  • Infinitive
  • Registratie: Maart 2001
  • Laatst online: 25-09-2023
Een invariant is een eigenschap die, als hij waar is aan het begin van het uitvoeren van een stukje code, ook waar is aan het einde van een stukje code waar is. Het is dus een eigenschap die nog steeds geldt na het uitvoeren van het stukje code (niet noodzakelijk tussendoor).

Dit kan je zien aan {P && B} S {P}. De conditie P is waar bij aanvang van S (zelfs nog wat meer, namelijk ook nog B ), en ook nog aan het eind van het uitvoeren van S.

Een loop-invariant is typisch iets wat je bij loops tegenkomt. Je bewijst dat iets waar is bij aanvang van een iteratie, aan het einde van een iteratie, en je bewijst dat het aantal iteraties eindig is. Dan kan je concluderen dat de loop termineerd met die conditie.

Hah, ik ben niet helemaal spuitelf, want die conditie P hoeft niet te blijven gelden gedurende de uitvoering van S. Dus de invariant geldt niet altijd :P

[ Voor 13% gewijzigd door Infinitive op 03-01-2005 22:20 ]

putStr $ map (x -> chr $ round $ 21/2 * x^3 - 92 * x^2 + 503/2 * x - 105) [1..4]


Acties:
  • 0 Henk 'm!

Anoniem: 118860

Er zijn -- voor zover ik weet -- twee verschillende typen invarianten: lusinvarianten en klasseinvarianten.

Op school zul je voornamelijk te maken hebben met lusinvarianten; dat is een bewering die geldt aan het begin en eind van de luscode, ongeacht de waarde van de herhalingsconditie. Hij geldt dus vóór de eerste iteratie, tussen elke iteratie, en nà de laatste iteratie.

Tussendoor hoeft hij niet te gelden. Dat is nogal logisch, want het kan zijn dat je meer dan 1 statement nodig hebt om de invariant te waarborgen (dat is ook vaak zo), en dan zou de invariant tussen die statements niet gelden.

Lusinvarianten worden vaak uitgedrukt in termen van lokale variabelen die belangrijk zijn in de lus.

Een schoolboekvoorbeeldje erbij: een algoritme om het maximum uit een lijst van integers te vinden. In het algoritme gaat een array a met lengte N, en we willen aan het eind het grootste getal van die array in r hebben.

Wat je wilt bereiken (eindconditie) is:
code:
1
R: r = (MAX i: 0 <= i < N: a[i])


Een goede invariant bedenken is niet makkelijk, maar een standaardmethode die we hier kunnen gebruiken is `vervang de constante (N) door een variabele (n)'.

De invariant wordt dan:
code:
1
INV: r = (MAX i: 0 <= i < n: a[i])


Wat dit effectief betekent is dat in elke iteratie de huidige waarde van r niet iets zegt over de hele array, maar slechts over een deel van de array. Door dit deel steeds groter te maken tot het uiteindelijk gelijk is aan de hele array, kom je tot een algoritme dat het gevraagde probleem berekent.

In dit geval betekent dat, laat n bij 0 beginnen en verhoog hem elke iteratie met 1 totdat de bovengrens van de array bereikt is.

code:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
con N : int
var a : array[0..N) of int
var r : int

n := 0
r := -ONEINDIG 

{ INV }
while n < N do
  if a[n] > r then
    r = a[n]
  fi

  n := n + 1  
  { INV }
od

{R}


Een makkelijke manier om te controleren of je invariant in elk geval een beetje klopt: als alles goed gaat, moet de invariant gecombineerd met de negatie van de herhalingsconditie (immers, aan het eind ben je klaar met de lus uitvoeren) samen de eindconditie vormen.

In dit voorbeeld is dat ook zo, immers

code:
1
INV /\ n = N => R


(Dit is een beetje kort door de bocht omdat ¬(n < N) strikt gesproken natuurlijk gelijk is aan n >= N en niet n = N, maar je kunt eenvoudig zien (en ook bewijzen) dat n nooit groter dan N zal worden)

Overigens ben je hiermee nog niet klaar met het bewijzen van dit algoritme, maar de rest gaat allemaal niet over invarianten (en als ik eerlijk moet zijn weet ik ook niet meer precies hoe het gaat :+).


Dan heb je nog klasseinvarianten: die kunnen in OOP gebruikt worden om iets te zeggen over de correctheid van klassen. Klasseinvarianten dienen te gelden vóór en na de aanroep van een publieke methode op die klasse. Een voorbeeld van een klasseinvariant is bijvoorbeeld (voor een container object):

code:
1
Size = 0 <=> IsEmpty()


Om maar iets te noemen.

Maar in de praktijk geloof ik niet dat je ze veel tegen komt; ik heb alleen de taal Eiffel gezien die er ondersteuning voor heeft (en die heeft ook ondersteuning voor pre- en postcondities, en voor lusinvarianten... mmmm B))

Acties:
  • 0 Henk 'm!

  • Robtimus
  • Registratie: November 2002
  • Laatst online: 19:39

Robtimus

me Robtimus no like you

Anoniem: 118860 schreef op dinsdag 04 januari 2005 @ 01:37:
(Dit is een beetje kort door de bocht omdat ¬(n < N) strikt gesproken natuurlijk gelijk is aan n >= N en niet n = N, maar je kunt eenvoudig zien (en ook bewijzen) dat n nooit groter dan N zal worden)
Yep, extra invariant: 0 <= n <= N ;)

Vergeet trouwens ook niet dat er nog een bewijsverplichting bestaat: de eindiging van de loop.

More than meets the eye
There is no I in TEAM... but there is ME
system specs


Acties:
  • 0 Henk 'm!

  • Ivo
  • Registratie: Juni 2001
  • Laatst online: 14-01 18:01

Ivo

Voor de volledigheid:

Terminering van de loop kan je bewijzen door een variante functie in termen van programmavariabelen te vinden die na elke loop een kleinere waarde heeft dan zijn vorige waarde en ( als geldt 0<=N ) dat de waarde nooit kleiner is dan 0.

Volgende week zaterdag tentamen hierover. Wordt nog pittig.

Edit: In OneOfBorg's voorbeeld redelijk standaard: vf = N-n

[ Voor 10% gewijzigd door Ivo op 04-01-2005 12:53 ]


Acties:
  • 0 Henk 'm!

  • Robtimus
  • Registratie: November 2002
  • Laatst online: 19:39

Robtimus

me Robtimus no like you

Ivo schreef op dinsdag 04 januari 2005 @ 12:52:
Voor de volledigheid:

Terminering van de loop kan je bewijzen door een variante functie in termen van programmavariabelen te vinden die na elke loop een kleinere waarde heeft dan zijn vorige waarde en ( als geldt 0<=N ) dat de waarde nooit kleiner is dan 0.

Volgende week zaterdag tentamen hierover. Wordt nog pittig.

Edit: In OneOfBorg's voorbeeld redelijk standaard: vf = N-n
Als TU/e'er hoor je te weten dat je voor dat geval mag schrijven "standaard eindiging" ;)

of iig vanaf volgend trimester dan :P

[ Voor 3% gewijzigd door Robtimus op 04-01-2005 13:17 ]

More than meets the eye
There is no I in TEAM... but there is ME
system specs


Acties:
  • 0 Henk 'm!

Anoniem: 118860

IceManX schreef op dinsdag 04 januari 2005 @ 08:59:
[...]
Yep, extra invariant: 0 <= n <= N ;)

Vergeet trouwens ook niet dat er nog een bewijsverplichting bestaat: de eindiging van de loop.
Ohja, dat was het :p.

En ik had al gezegd dat mijn bewijs niet volledig was :).
IceManX schreef op dinsdag 04 januari 2005 @ 13:17:
Als TU/e'er hoor je te weten dat je voor dat geval mag schrijven "standaard eindiging" ;)
of iig vanaf volgend trimester dan :P
Dat zal het dan zijn, want wij mochten dat niet... althans niet voor het vak waarin dit allemaal uitgelegd werd.

Bij latere vakken was het wel voldoende om `triviaal' op te schrijven, dus daar kon je jezelf nog een heel eind mee door het tentamen bluffen B).

[ Voor 49% gewijzigd door Anoniem: 118860 op 04-01-2005 13:46 ]


Acties:
  • 0 Henk 'm!

  • Ivo
  • Registratie: Juni 2001
  • Laatst online: 14-01 18:01

Ivo

IceManX schreef op dinsdag 04 januari 2005 @ 13:17:
[...]
Als TU/e'er hoor je te weten dat je voor dat geval mag schrijven "standaard eindiging" ;)

of iig vanaf volgend trimester dan :P
Ik ben sowieso nog de bits 'n pieces op orde aan het krijgen. Alles afzonderlijk begrijp ik wel, maar om alles toe te passen om een programma van 0 af te schrijven moet ik nog eens goed naar kijken.

Acties:
  • 0 Henk 'm!

  • sopsop
  • Registratie: Januari 2002
  • Laatst online: 16-05 16:55

sopsop

[v] [;,,;] [v]

Even spuit 11,vandale meldt:

in·va·ri·ant1 (de ~ (m.))
1 onveranderd blijvende grootheid

in·va·ri·ant2 (bn.)
1 onveranderlijk

m.a.w. wat je ook doet in je loop, de invariant moet geldig blijven: onveranderlijk.

[ Voor 25% gewijzigd door sopsop op 04-01-2005 16:18 ]


Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Alarmnummer schreef op maandag 03 januari 2005 @ 22:13:
Ik neem aan dat je weet wat design by contract is?

Een invariant is iets dat altijd geld.
Bv... als ik geld overmaak van jouw rekening, naar mijn rekening... dan moet voor en na deze actie gelden: het totaal aan geld is gelijk.

Een preconditie = iets dat moet gelden als je ergens aan begint..

Een postconditie = iets dat moet gelden als je er mee klaar bent.
design by contract :?
Nog nooit van die term gehoord. Zal wel hetzelfde zijn, als waar ik nu mee bezig ben. Het boek heet gewoon: Ontwerpen van algoritmen.

Acties:
  • 0 Henk 'm!

  • Grijze Vos
  • Registratie: December 2002
  • Laatst online: 28-02 22:17
IceManX schreef op dinsdag 04 januari 2005 @ 13:17:
[...]
Als TU/e'er hoor je te weten dat je voor dat geval mag schrijven "standaard eindiging" ;)

of iig vanaf volgend trimester dan :P
Feijen heeft liever gewoon:

"vf: N-n" ;)

("triviaal" bestaat uit nog meer letters man.)

(Afgelopen trimester nog een 8 gescoord voor Ontwerp van Algoritmen 2. De uitgebreidere Bachelor-variant van Programmeren 2, btw.)

[ Voor 9% gewijzigd door Grijze Vos op 04-01-2005 20:41 ]

Op zoek naar een nieuwe collega, .NET webdev, voornamelijk productontwikkeling. DM voor meer info


Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Anoniem: 118860 schreef op dinsdag 04 januari 2005 @ 01:37:
Er zijn -- voor zover ik weet -- twee verschillende typen invarianten: lusinvarianten en klasseinvarianten.

Op school zul je voornamelijk te maken hebben met lusinvarianten; dat is een bewering die geldt aan het begin en eind van de luscode, ongeacht de waarde van de herhalingsconditie. Hij geldt dus vóór de eerste iteratie, tussen elke iteratie, en nà de laatste iteratie.

Tussendoor hoeft hij niet te gelden. Dat is nogal logisch, want het kan zijn dat je meer dan 1 statement nodig hebt om de invariant te waarborgen (dat is ook vaak zo), en dan zou de invariant tussen die statements niet gelden.

Lusinvarianten worden vaak uitgedrukt in termen van lokale variabelen die belangrijk zijn in de lus.

Een schoolboekvoorbeeldje erbij: een algoritme om het maximum uit een lijst van integers te vinden. In het algoritme gaat een array a met lengte N, en we willen aan het eind het grootste getal van die array in r hebben.

Wat je wilt bereiken (eindconditie) is:
code:
1
R: r = (MAX i: 0 <= i < N: a[i])


Een goede invariant bedenken is niet makkelijk, maar een standaardmethode die we hier kunnen gebruiken is `vervang de constante (N) door een variabele (n)'.

De invariant wordt dan:
code:
1
INV: r = (MAX i: 0 <= i < n: a[i])


Wat dit effectief betekent is dat in elke iteratie de huidige waarde van r niet iets zegt over de hele array, maar slechts over een deel van de array. Door dit deel steeds groter te maken tot het uiteindelijk gelijk is aan de hele array, kom je tot een algoritme dat het gevraagde probleem berekent.

In dit geval betekent dat, laat n bij 0 beginnen en verhoog hem elke iteratie met 1 totdat de bovengrens van de array bereikt is.

code:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
con N : int
var a : array[0..N) of int
var r : int

n := 0
r := -ONEINDIG 

{ INV }
while n < N do
  if a[n] > r then
    r = a[n]
  fi

  n := n + 1  
  { INV }
od

{R}


Een makkelijke manier om te controleren of je invariant in elk geval een beetje klopt: als alles goed gaat, moet de invariant gecombineerd met de negatie van de herhalingsconditie (immers, aan het eind ben je klaar met de lus uitvoeren) samen de eindconditie vormen.

In dit voorbeeld is dat ook zo, immers

code:
1
INV /\ n = N => R


(Dit is een beetje kort door de bocht omdat ¬(n < N) strikt gesproken natuurlijk gelijk is aan n >= N en niet n = N, maar je kunt eenvoudig zien (en ook bewijzen) dat n nooit groter dan N zal worden)

Overigens ben je hiermee nog niet klaar met het bewijzen van dit algoritme, maar de rest gaat allemaal niet over invarianten (en als ik eerlijk moet zijn weet ik ook niet meer precies hoe het gaat :+).


Dan heb je nog klasseinvarianten: die kunnen in OOP gebruikt worden om iets te zeggen over de correctheid van klassen. Klasseinvarianten dienen te gelden vóór en na de aanroep van een publieke methode op die klasse. Een voorbeeld van een klasseinvariant is bijvoorbeeld (voor een container object):

code:
1
Size = 0 <=> IsEmpty()


Om maar iets te noemen.

Maar in de praktijk geloof ik niet dat je ze veel tegen komt; ik heb alleen de taal Eiffel gezien die er ondersteuning voor heeft (en die heeft ook ondersteuning voor pre- en postcondities, en voor lusinvarianten... mmmm B))
Bedankt voor je uitleg. (jullie allemaal bedankt)
Dat van die lusinvariant, dat is precies wat behandeld wordt in de HP1 module. Ik zal je verhaal nog een keer aandachtig doorlezen. In klasseinvarianten ga ik me maar nog niet verdiepen, dat komt wel in de volgende model HP2, die over OOP gaat.

Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Ivo schreef op dinsdag 04 januari 2005 @ 12:52:
Voor de volledigheid:

Terminering van de loop kan je bewijzen door een variante functie in termen van programmavariabelen te vinden die na elke loop een kleinere waarde heeft dan zijn vorige waarde en ( als geldt 0<=N ) dat de waarde nooit kleiner is dan 0.
En nu in gewoon nederlands :) (ik weet inmiddels al wat een invariant is)
In dat boek wat ik gebruik, staan ook van dit soort zinnen. Die je eerst 3 keer moet lezen voordat je het begint te begrijpen.

Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
boppert schreef op dinsdag 04 januari 2005 @ 16:18:
Even spuit 11,vandale meldt:

in·va·ri·ant1 (de ~ (m.))
1 onveranderd blijvende grootheid

in·va·ri·ant2 (bn.)
1 onveranderlijk

m.a.w. wat je ook doet in je loop, de invariant moet geldig blijven: onveranderlijk.
Slim, om het in een woordenboek op te zoeken. Had ik in eerste instantie helemaal niet aan gedacht.

Acties:
  • 0 Henk 'm!

Anoniem: 42145

Anoniem: 124228 schreef op maandag 03 januari 2005 @ 22:05:
{P} //preconditie
while B do
begin
{P && B}
S //opdracht
{P}
end
{P && !B}
{Q} //postconditie
In het algemeen is dit voorbeeld mischien niet helemaal volledig. Je zet {P} hier als preconditie neer terwijl dit hier eigenlijk de invariant is en niet perse de preconditie.

In het algemeen heb je dus:

{Q} // preconditie
{P} //invariant
while B do
begin
{P && B}
S //opdracht
{P}
end
{P && !B}
{R} //postconditie
[/quote]

Je bewijst het programma door Q via S met R te verbinden. Concreet houdt dat in dat je de logische implicatie moet bewijzen dat Q => P en dat P && !B => R. Als er geen specificieke {Q} is kun je true gebruiken.


Het klinkt zo allemaal redelijk te doen, maar nu zijn Q, P, B en R echter geen simpele booleans in het algemeen maar kunnen een grote relatie zijn. Iedereen die een vak over Logica heeft gevolgt weet dat zelfs simpel ogende implicaties niet geheel triviaal te bewijzen zijn. Alleen al die implicaties bewijzen is enorm rottig, zeker als je niet al te thuis bent in de logica.

Daar komt dan nog het bewijs van de loop, en dus elke statement daarin stuk voor stuk bij. Globaal begin je daarmee door {P} achter het laatste statement in de loop body te plaatsen en dan 'omhoog' te bewijzen, regel voor regel. Je relatie {Pn} wordt daarbij steeds complexer. Als je dan eenmaal bij omhooggewerkt hebt voorbij het eerste statement mag je nog eens de implicatie {P && B} => {Px} bewijzen. Zelfs bij enorm triviaal ogende loops levert dat al een flinke expressie op die echt practisch niet te bewijzen is (voor mij dan ;) ). Dan nog eens de geheeltallige expressie t vinden om de eindigheid van de loop mee te bewijzen. Een simpele loop met 2 statements kan al snel enkele A4'tjes (!) aan volledig uitgeschreven bewijs opleveren.

Nee, gemakkelijk is het niet :) Voor elke gangbare vorm van software development is een correctheids bewijs eigenlijk niet uitvoerbaar. Te meer niet omdat bij elke verandering in je code het weer overnieuw gedaan mag worden.

Acties:
  • 0 Henk 'm!

  • Ivo
  • Registratie: Juni 2001
  • Laatst online: 14-01 18:01

Ivo

Anoniem: 124228 schreef op dinsdag 04 januari 2005 @ 20:46:
[...]

En nu in gewoon nederlands :) (ik weet inmiddels al wat een invariant is)
In dat boek wat ik gebruik, staan ook van dit soort zinnen. Die je eerst 3 keer moet lezen voordat je het begint te begrijpen.
Meestal heb je als guard van de repetitie iets in de zin van N != n. (Denk aan een array die loopt van 0 tot en zonder N, die je doorlooopt met een variabele n) Deze repetitie eindigt pas zodra geldt N = n. Om aan te tonen dat dit ooit voor komt moet je een functie vinden met variabelen n, N en willekeurige andere programmavariabelen die na elke uitvoering van de loop statements een kleinere waarde heeft dan de waarde ervoor. Stel nou dat je een loop hebt met als guard N != n en bij elke uitvoering van de loop verhoog je n met 1, dan heb je zo'n functie met vf = N - n (vf staat voor variante functie, maar dat is niet belangrijk hier). Na elke uitvoering van de loop wordt n 1 groter en dus N - n 1 kleiner. Dat klopt dus. Het is ook nog belangrijk dan N - n nooit kleiner dan 0 wordt (anders zou tijdens het verhogen van n over de conditie N = n heen gesprongen worden). Daarom heb je meestal als extra invariant 0 <= n <= N. Dan kan N - n nooit kleiner dan 0 worden.

Ik hoop dat dit iets duidelijker is. Ik vind het best moeilijk om uit te leggen. Meestal een teken dat ik er zelf ook nog flink wat tijd aan moet besteden.

Edit: Zo ontzettend helder ben ik ook weer niet, als het wartaal is wat ik heb geschreven dan zal ik het morgen verbeteren.

[ Voor 5% gewijzigd door Ivo op 05-01-2005 02:03 ]


Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Ivo schreef op woensdag 05 januari 2005 @ 02:02:
[...]

Ik hoop dat dit iets duidelijker is. Ik vind het best moeilijk om uit te leggen. Meestal een teken dat ik er zelf ook nog flink wat tijd aan moet besteden.

Edit: Zo ontzettend helder ben ik ook weer niet, als het wartaal is wat ik heb geschreven dan zal ik het morgen verbeteren.
Het was ook eigenlijk meer als grapje bedoelt. iig bedankt voor je uitleg.

[ Voor 4% gewijzigd door Anoniem: 124228 op 05-01-2005 07:59 ]


Acties:
  • 0 Henk 'm!

Anoniem: 121839

Anoniem: 124228 schreef op dinsdag 04 januari 2005 @ 20:46:
[...]

En nu in gewoon nederlands :) (ik weet inmiddels al wat een invariant is)
In dat boek wat ik gebruik, staan ook van dit soort zinnen. Die je eerst 3 keer moet lezen voordat je het begint te begrijpen.
Als je die zin al moeilijk vond dan moet je dus echt geen universiteit gaan doen! :) (niet dat je hebt gezegd dat je dat wilt hoor, maar gewoon als losse opmerking). De zinnen die daar gebruikt worden om correctheids bewijzen te defineren gaan echt nog 100 keer zo ver. Vergeleken bij dat is de zin die jij moeilijk vond een gemakkelijke informele omschrijving ;)

Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
Anoniem: 121839 schreef op woensdag 05 januari 2005 @ 10:20:
[...]


Als je die zin al moeilijk vond dan moet je dus echt geen universiteit gaan doen! :) (niet dat je hebt gezegd dat je dat wilt hoor, maar gewoon als losse opmerking). De zinnen die daar gebruikt worden om correctheids bewijzen te defineren gaan echt nog 100 keer zo ver. Vergeleken bij dat is de zin die jij moeilijk vond een gemakkelijke informele omschrijving ;)
Dat was ik ook niet van plan. Eerst m'n AMBI diploma halen, daarna misschien voor m'n ing titel gaan, maar dat zie ik nog wel.

Even on topic.
Dus in de praktijk wordt deze methode bijna nooit toegepast, wat ik ook al dacht, ik ben al zo'n 5 jaar vrij intensief met programmeren bezig en voordat ik aan deze module begon had ik er nog nooit van gehoord.

Wat is dan het nut van dit geneuzel? Ik denk dat het goed is voor je inzicht en dat je soms sneller en beter tot een goed algoritme komt. Bijvoorbeeld bij het ontwerpen van zoekalgoritmen, den ik dat je hier wel wat aan kan hebben. Wat je ook leert is het adv een pre- en postconditie berekenen van opdrachten.

Acties:
  • 0 Henk 'm!

Anoniem: 42145

Anoniem: 124228 schreef op woensdag 05 januari 2005 @ 20:10:
[...]

Wat is dan het nut van dit geneuzel?
Het nut is enorm: totale inzicht in het gedrag van je software. Nooit meer aparte gevallen hoeven te testen om er dan in produktie achter te komen dat er een geval optreed waar je code toch fout op gaat.

In de praktijk betekent dit overigens nog steeds niet bug vrije software. Het betekent alleen dat tenminste de condities gelden die jij bewezen hebt. Deze condities moeten natuurlijk ook nog eens kloppen met wat de bedoeling is. Ik kan dus wel mooi bewijzen dat na een bepaalde serie statements beginnend met n>0 geldt dat (x-1)^2 > n >= y+3 < (z-2x )/4 etc etc. maar als dat eigenlijk toch niet de bedoeling was van de software en dan blijkt pas uit gedrag van je software door klachten van gebruikers, dan heb je alsnog een feitelijke bug.

Je gebruikt het voornamelijk voor kleine, specificieke algorithmen, bijvoorbeeld voor de berekening van de geheeltallige vierkantswortel oid (dit is 3 regels code). Het zijn meestal wiskundige functies waarbij je dan bewijst dat je code ook overeenkomt met het wiskundig equivalent van die functie. Andere dingen zijn mischien dingen als code om de sinus te berekenen, dat je bewijst dat jouw code echt altijd de sinus is. Ik weet nog uit de oude tijd dat vroegere implementaties voor extreem grote hoeken nooit de goede waarden gaven. Maar nu zit ik echt een beetje te gokken of dit inderdaad de practische toepassing is. Je gebruikt het iniedergeval niet om iets als een kernel formeel of een spel formeel te bewijzen.

Acties:
  • 0 Henk 'm!

  • naruto
  • Registratie: Augustus 2001
  • Laatst online: 16-08-2020
offtopic:
ik ben al een tijdje op zoek naar een goed boek over algoritmes (design and analyzing). Ik heb het volgende kunnen vinden:

- Introduction to Algorithms, Second Edition
by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein
schijnt een must have te zijn. Geschikt als leer- en naslag werk maar wel erg technisch.

- Introduction to the Design and Analysis of Algorithms
by Anany V. Levitin
de auteur beschrijft een aantal technieken om een algoritme te kunnen ontwerpen etc.

graag zal ik willen weten of deze twee boeken aanraders zijn:)

en verder zal ik graag willen weten of het volgende boek een aanrader is:

-Programming Game AI by Example with CDROM
Matt Buckland
--------------------------------

ontopic:
in clasic data structures in java :
in invariant is niet meer dan een comment. het beschrijft de status van een berekening op het punt waar de comment tijdens de execution zich bevindt.

Acties:
  • 0 Henk 'm!

Anoniem: 118860

b schreef op woensdag 05 januari 2005 @ 22:43:
ontopic:
in clasic data structures in java :
in invariant is niet meer dan een comment. het beschrijft de status van een berekening op het punt waar de comment tijdens de execution zich bevindt.
Daar ben ik het niet mee eens. In mijn ogen heet dat een assertie.

Een invariant hoort bij een bepaalde softwareconstructie en zegt iets over de onveranderlijke eigenschappen van die constructie. Een invariant staat niet `zomaar ergens in de code'.

[ Voor 6% gewijzigd door Anoniem: 118860 op 05-01-2005 22:47 ]


Acties:
  • 0 Henk 'm!

Anoniem: 124228

Topicstarter
b schreef op woensdag 05 januari 2005 @ 22:43:
offtopic:
ik ben al een tijdje op zoek naar een goed boek over algoritmes (design and analyzing). Ik heb het volgende kunnen vinden:

- Introduction to Algorithms, Second Edition
by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein
schijnt een must have te zijn. Geschikt als leer- en naslag werk maar wel erg technisch.

- Introduction to the Design and Analysis of Algorithms
by Anany V. Levitin
de auteur beschrijft een aantal technieken om een algoritme te kunnen ontwerpen etc.

graag zal ik willen weten of deze twee boeken aanraders zijn:)

en verder zal ik graag willen weten of het volgende boek een aanrader is:

-Programming Game AI by Example with CDROM
Matt Buckland
--------------------------------

ontopic:
in clasic data structures in java :
in invariant is niet meer dan een comment. het beschrijft de status van een berekening op het punt waar de comment tijdens de execution zich bevindt.
Heb je al op Amazon gekeken?
Bij Introduction to Algorithms, Second Edition staat een uitgebreide beschrijving en veel customers reviews.
Op dit moment ben ik bezig in het boek "Het ontwerpen van algoritmen" van Kaldewaij, waarvan je een kopie (het boek is niet maar te krijgen) krijgt van Exin als je de HP1 module gaat doen.
Introduction to Algorithms lijkt me een goed vervolg hierop, maar laat ik eerst maar eens HP1 afmaken.
Pagina: 1