mboost-dp1
SXC - theRIAA
#2 Det kan de da sagtens. For så sender de jo bare Isabelle på opgaven igen og laver et nyt bevis.
Det fantastiske i nyheden er jo netop at man kan BEVISE at programmet er fejlfrit og ikke bare teste det lidt hist og pist som man normalt er nødt til at nøjes med at gøre.
Det fantastiske i nyheden er jo netop at man kan BEVISE at programmet er fejlfrit og ikke bare teste det lidt hist og pist som man normalt er nødt til at nøjes med at gøre.
Jeg sidder og prøver at forstå betydnignen af det her.
Hvis vi nærmer os et system, der matematisk kan validere, at et system er fejlfrit, så må man kunne nå ufatteligt langt ved at køre det på operativsystemet og de få grundlæggende libraries, som det meste software er baseret på.
Dog må fejlfrit dække over det rent software-mæssige, for hvad sker der, hvis man har en driver, der modtager forkert input fra hardware. Tager den højde for det?
Kan Isabella også fortælle hvilke dele af koden, der giver problemer ifht. beviset eller kommer den bare til sandt/falsk? (Jeg går ud fra, at den giver nogle hints siden seL4 er valideret - det er jo en umulig opgave med kun sandt/falsk).
Jeg ved, at det her er lidt langt ude i fremtiden, men det er da interessant nok at tænke over...
Hvis vi nærmer os et system, der matematisk kan validere, at et system er fejlfrit, så må man kunne nå ufatteligt langt ved at køre det på operativsystemet og de få grundlæggende libraries, som det meste software er baseret på.
Dog må fejlfrit dække over det rent software-mæssige, for hvad sker der, hvis man har en driver, der modtager forkert input fra hardware. Tager den højde for det?
Kan Isabella også fortælle hvilke dele af koden, der giver problemer ifht. beviset eller kommer den bare til sandt/falsk? (Jeg går ud fra, at den giver nogle hints siden seL4 er valideret - det er jo en umulig opgave med kun sandt/falsk).
Jeg ved, at det her er lidt langt ude i fremtiden, men det er da interessant nok at tænke over...
f-style (6) skrev:Så skal det bare skrives så det kunne analyserer hele styresystemer :).
Ville være sejt hvis det rent faktisk ville virke, så kunne windows, linux, bsd, unix ect. køres igennem :). Men det er nok bare utopi, da der er alt for meget kode at skulle analyserer.
Testen afslører kun om der er programmatiske fejl som kan forårsage nedbrud ved runtime. Der testes ikke for brugerfejl.
Et program der er fejlfrit vil stadig fejle hvis brugeren er tilstrækkelig dum og forsøger at udføre handlinger der ikke kan lade sig gøre.
#7 / #8: Ikke nødvendigvis. Hvis et program er valideret, så er det valideret - under alle de former for input der er mulige i modellen.
Hvis man fx har et tastatur som input-enhed, så er der ingen input herfra der vil kunne få et valideret program til at fejle - i hvert fald så længe man ikke har simplificeret testen ved at begrænse mulige input til de "mest sandsynlige" (fx sat en øvre grænse for hvor hurtigt tastaturet kan spytte data ud eller lignende, eller gået ud fra at tastaturet altid giver gyldige tegn).
Hvis man fx har et tastatur som input-enhed, så er der ingen input herfra der vil kunne få et valideret program til at fejle - i hvert fald så længe man ikke har simplificeret testen ved at begrænse mulige input til de "mest sandsynlige" (fx sat en øvre grænse for hvor hurtigt tastaturet kan spytte data ud eller lignende, eller gået ud fra at tastaturet altid giver gyldige tegn).
TrolleRolle (3) skrev:#2 Det kan de da sagtens. For så sender de jo bare Isabelle på opgaven igen og laver et nyt bevis.
Det fantastiske i nyheden er jo netop at man kan BEVISE at programmet er fejlfrit og ikke bare teste det lidt hist og pist som man normalt er nødt til at nøjes med at gøre.
1. Uden at vide det præcist vil jeg antage at der går temmelig lang tid på at beregne sådan et bevis.
2. Det er ikke nyt. Lignende beviser af micro kerner er lavet i 70'erne. Problemet er hvad man vil bevise. Jeg har forsøgt mig lidt med at opstilning af matematiske krav til kode. Det er absolut ikke trivielt!
3. Med mindre Isabelle's egen kode er bevist, har de ikke bevist en hat (jeg kan her afsløre at det er den ikke men de mener den er meget gennemtestet :-) ).
4. Det er ikke bevist at systemet er sikkert. Det eneste isabelle kan bevise er at systemet overholder en række matematisk opstillede krav.
Hvis man siger at systemet er sikkert så antager man samtidig at rækken af opstillede krav (brugernes input til isabelle) er fejlfri og at de matematiske krav beskriver alle aspekter af "sikkerhed" perfekt.
Da jeg læste datalogi, havde vi et fag der hed Matematik og Beregninger, som var et matematisk system udviklet af D.Sc Klaus Grue der kunne bevise programmer.. Absolut ikke noget nyt, I flere år et 1 semesters fag på Datalogi ved KU...
http://www.diku.dk/hjemmesider/ansatte/grue/cv.htm...
http://www.diku.dk/hjemmesider/ansatte/grue/cv.htm...
Et korrekthedsbevis er ikke noget bevis for, at processoren altid virker. Det kan kun bevise påstande, som at ... hvis de enkelte operationer har disse givne egenskaber, så har sammensætningen af operationer nogle andre egenskaber.
Hvis antagelserne om de enkelte operationer ikke holder stik (som f.eks. ved hardwarefejl pga. overophedning osv) så kan beviset ikke bruges til noget.
F.eks. kan man se i "stack dumps" fra mange fejl, som f.eks. rapporteres til Microsoft, at processoren har gjort noget, der ikke burde kunne lade sig gøre.
Hvis antagelserne om de enkelte operationer ikke holder stik (som f.eks. ved hardwarefejl pga. overophedning osv) så kan beviset ikke bruges til noget.
F.eks. kan man se i "stack dumps" fra mange fejl, som f.eks. rapporteres til Microsoft, at processoren har gjort noget, der ikke burde kunne lade sig gøre.
#4 I tillæg til #5 kunne man tilføje at det de laver er en over approximation (eller underapproximation), det vil sige de vurderer en given egenskab for en større mængde tilstande end programmet kan komme i. Da egenskaben kan bevises for en mængde af tilstande, hvor mængden af tilstande programmet kan komme i er indeholdt, må det være indeholdt i programmet. Søger vi, uden at finde, efter tilstanden BAD i en overapproximation, findes den ej heller i en delmængde af den gennemsøgte tilstand.
Samme principt holder for under approximationer - hvis tilstanden BAD _findes_ i en underapproximation, i en delmængde af programmets tilstande, findes den også i programmets tilstande.
Disse approximationer gør spørgsmålet afgørbart. Tænk på din compiler hvis du laver:
int a, b;
a =1;
if(a==1) b=0;
a=b;
simple analyser vil fortælle dig at b ikke er initialiseret før brug, selvom vi vil kunne se at den altid er.
Samme principt holder for under approximationer - hvis tilstanden BAD _findes_ i en underapproximation, i en delmængde af programmets tilstande, findes den også i programmets tilstande.
Disse approximationer gør spørgsmålet afgørbart. Tænk på din compiler hvis du laver:
int a, b;
a =1;
if(a==1) b=0;
a=b;
simple analyser vil fortælle dig at b ikke er initialiseret før brug, selvom vi vil kunne se at den altid er.
#0
For de nysgerrige er der flere detaljer i linkesene nederst på:
http://ertos.nicta.com.au/research/l4.verified/
For de nysgerrige er der flere detaljer i linkesene nederst på:
http://ertos.nicta.com.au/research/l4.verified/
#4 << Uddybning af #5: Halting-problemet beskriver intet om (algoritmer vedrørende) programmers "korrekthed". Halting-problemet beskæftiger sig udelukkende med algoritmer vedr. programmers afslutning og siger, at der ikke kan skrives én generel algoritme, som viser, hvorvidt et vilkårligt program vil afslutte.
Således taler problemet ikke imod at udvikle en sådan algoritme for hvert tænkeligt program.
#14 << Hvad mener du med, at "b" ikke er initialiseret "før brug"? Simpel analyse i mit hoved fortæller mig, at du initialiserer variablene "a" og "b" på første linie ved "int a, b" - og jeg gætter, at du med "brug" mener det øjeblik, hvor "b" tildeles værdi..?
Mener du, at compileren ikke internt initialiserer "b", før den ser, at variablen rent faktisk benyttes, og - i bekræftende fald - hvad er relevansen?
Således taler problemet ikke imod at udvikle en sådan algoritme for hvert tænkeligt program.
#14 << Hvad mener du med, at "b" ikke er initialiseret "før brug"? Simpel analyse i mit hoved fortæller mig, at du initialiserer variablene "a" og "b" på første linie ved "int a, b" - og jeg gætter, at du med "brug" mener det øjeblik, hvor "b" tildeles værdi..?
Mener du, at compileren ikke internt initialiserer "b", før den ser, at variablen rent faktisk benyttes, og - i bekræftende fald - hvad er relevansen?
#18 << Det var ikke nogen forklaring; venligst uddyb..?
Jeg savner især svar på
- "Hvad mener du med, at "b" ikke er initialiseret "før brug"?"
- "Mener du, at compileren ikke internt initialiserer "b", før den ser, at variablen rent faktisk benyttes,"
og
- "hvad er relevansen?"
Jeg savner især svar på
- "Hvad mener du med, at "b" ikke er initialiseret "før brug"?"
- "Mener du, at compileren ikke internt initialiserer "b", før den ser, at variablen rent faktisk benyttes,"
og
- "hvad er relevansen?"
#17 ok. I mit hovede er "int a, b;" det man kalder 'erklæringen' (det nogle (fejlagtigt?) kalder deklareringen) af variablerne, hvor tilskrivningen af værdier til disse variable vil være en initialisering.
Iflg denne "definition" vil de være uinitialiserede da de ikke har fået tilskrevet en værdi endnu, (eller set som uinitialiserede, f.eks. i sprog som Java - ihvertfald med den compiler jeg har ved hånde, eclipse, brokke sig lidt (om JVM specifikationen siger noget om initialisering af variable er imho ligegyldigt, det var for illustration, uanset hvor dårligt eksemplet er)).
Min pointe var, at give et bud på en over/under approximation eller "safe approximation" eller hvad man vælger at kalde det, som uddybende forklaring af tidligere.
Et eksempel, hvor alle tilstande programmet faktisk kan nå i er sikre, men hvor man har en statisk analyse der tager en mængde tilstande der er skarpt større end det faktiske tilstandsrum i.e. tager "else" branchen med, hvor variablen 'b' ikke er initialiseret. (I følge min til eksemplet hjemmestrikkede semantik )
Denne approximation gør at man kan appriximere sig frem til svar til hvad Rice's theorem siger ikke kan lade sig gøre (uafgørbare sprøgsmål).
Det kan meget vel være det ikke var det bedste eksempel, specielt hvis der manglede forklaring. Beklager hvis det var utydeligt, håber det er bedre nu.
Iflg denne "definition" vil de være uinitialiserede da de ikke har fået tilskrevet en værdi endnu, (eller set som uinitialiserede, f.eks. i sprog som Java - ihvertfald med den compiler jeg har ved hånde, eclipse, brokke sig lidt (om JVM specifikationen siger noget om initialisering af variable er imho ligegyldigt, det var for illustration, uanset hvor dårligt eksemplet er)).
Min pointe var, at give et bud på en over/under approximation eller "safe approximation" eller hvad man vælger at kalde det, som uddybende forklaring af tidligere.
Et eksempel, hvor alle tilstande programmet faktisk kan nå i er sikre, men hvor man har en statisk analyse der tager en mængde tilstande der er skarpt større end det faktiske tilstandsrum i.e. tager "else" branchen med, hvor variablen 'b' ikke er initialiseret. (I følge min til eksemplet hjemmestrikkede semantik )
Denne approximation gør at man kan appriximere sig frem til svar til hvad Rice's theorem siger ikke kan lade sig gøre (uafgørbare sprøgsmål).
Det kan meget vel være det ikke var det bedste eksempel, specielt hvis der manglede forklaring. Beklager hvis det var utydeligt, håber det er bedre nu.
Opret dig som bruger i dag
Det er gratis, og du binder dig ikke til noget.
Når du er oprettet som bruger, får du adgang til en lang række af sidens andre muligheder, såsom at udforme siden efter eget ønske og deltage i diskussionerne.
- Forside
- ⟨
- Forum
- ⟨
- Nyheder
Gå til bund