MagHam skrev:
Jag, som doktorerat inom verifiering av programvara men nu jobbar inom industrin med mjukvaruutveckling, känner att jag inte kan motstå att hoppa in här.lars_stefan_axelsson skrev:
Det är teoretiskt omöjligt att skapa en analyserare för alla program. Verifiering av programvara kräver att man tittar på begränsade klasser eller ett specifikt program för att det ska vara ens teoretiskt möjligt. Det är emellertid ointressant av två skäl:
1. För att kunna verifiera något som "buggfritt" behöver man en specifikation, med avseende på vilken det aktuella programmet skall vara buggfritt. Den specen är i stort sett omöjligt att ha i sin helhet för annat än näst intill triviala program. Modern mjukvaruutveckling är en iterativ process, inklusive designfasen.
2. Även om man har en specifikation, är det antagligen alldeles för krävande att verifiera, rent beräkningsmässigt. Om analysen är värre än O(n log n) eller liknande kan man nästan inte göra något i större skala.
Därmed inte sagt att man inte skall eftersträva korrekthet. Det görs dock med hjälp av
1. Ett bra IDE som fångar enkla fel tidigt
2. Code reviews eller regelrätt parprogrammering, eftersom det gäller att "given enough eyeballs, all bugs are shallow" som Raymond uttryckte det i The Cathedral and the Bazaar.
3. Tydligt ägandeskap av kod, så att man måste stå för vad man gör
Typ. Kommer säkert få mothugg från andra inom skrået, men det blottar man sig väl för när man skriver kl 0120 när man borde sovit för länge sen.
PS. Ja, jag känner till Spec#, Sing#, Java/ESC och allt vad dom heter. Fortfarande inget som används i någon meningsfull utsträckling på Google och liknande ställen, utan det är automatiserade tester och code reviews som gäller i kiseldalen.
Håller med om det mesta. Visste redan svaret på min frågajonmo skrev:
Har själv jobbat professionellt med mjukvaruutveckling sedan ca 1990 (i grunden elingenjör sedan läst systemvetenskap)
Min poäng var att vi ställer behörighetskrav som är ganska tydliga och formella på en elinstallation - men dimensionering av kretsar, programmering av styrsystem i industrin o s v kan släppa igenom många livsfarliga komponenter.
IDE verktyg och kodgranskning är bra, men missar en del logiska fel av t ex "state transition", eller transaktionella fel "vad händer om exekveringen avbryts just här".
Och då kan det i industrin handla om rörliga kolvar, påslagen spänning, ignorerade ändlägesbrytare etc etc.
Besserwisser
· Västra Götalands
· 9 834 inlägg
Du har PM.jonmo skrev:
Ja, Turing mfl visar ju det. Men det intressanta, om vi nu skall nörda ner oss är att Turings bevis är ett motsatsbevis. Och dessa leder ju oss sällan särskilt långt när det kommer till syntes. Klassen av program för vilka det faktiskt i teorin går att bevisa olika egenskaper är antagligen väldigt stor, och innehåller antagligen alla, eller iaf en stor del, av alla praktiskt användbara program. Särskilt för så "enkla" problem som styr och reglerproblemet. (Se exv. Lars Paretos arbete från nittotalet. Det är dock ett område det inte forskar så mycket inom. Vilket är både synd och underligt).jonmo skrev:
Tja, i högrisksystem så har man väldigt bra specifikationer. Jag tänker då på exv. flyg, kärnteknik osv. Med stor detaljrikedom och väl genomtänkta. Det är också "statiska" problem, som inte ändrat sig så värst. Men de blir för dyra att ta fram för allmänna system. Det är sant.jonmo skrev:
Det här är fortfarande ett problem. Iaf det generella problemet. Det är därför som man idag mera riktar in sig på specifika egenskaper hos program/system och ser isolerat på dessa.jonmo skrev:
Det är bra allmänna tips. Men om man vill nå nästa steg så vet vi lite mer idag.jonmo skrev:
Njae, inte riktigt. Statisk analys har gjort sitt intåg. Exv. via Coverity Så det är inte riktigt så entydigt som du säger. Bara nästan...jonmo skrev:
Åhå
Spännande vilka rävar som lurkar runt här då slänger in lite vedträn kring alla distribuerade system med microservices o circuit breakers o continious deployment som gör stageing mer eller mindre omöjligt.
Fastighets El är ändå något mindre komplex om man håller sig till normala situationer
Spännande vilka rävar som lurkar runt här då
slänger in lite vedträn kring alla distribuerade system med microservices o circuit breakers o continious deployment som gör stageing mer eller mindre omöjligt. Fastighets El är ändå något mindre komplex om man håller sig till normala situationer
Rocket är den nya svartaSkysodan skrev:Åhå
Spännande vilka rävar som lurkar runt här då
Fastighets El är ändå något mindre komplex om man håller sig till normala situationer
Jag var röris för många år sedan och när vi var upp vknden så hade tanten dragit el till vindsbelysningen direkt från centralen och fäst kabeln med mälor i takstolarna alltså sådana där vanliga man använder till stängsel och sedan hade hon sett att det var ju nästan som en tvättlina mellan takstolarna så hon hängde upp blöt tvätt på tork dä så kabeln hängde som en lian mellan takstolarna.
Inte värsta elkopplingen men kanske värsta elborrningen? En klant (läs:jag) mätte och mätte och mätte en gång till för att borra igenom en vägg. Synd att klanten inte tänkte på att det var ett litet kontor mellan...
Jag höll faktiskt på att göra en liknande fadäs idag.
Jag skulle ta hål för en canbus-kabel, in till ett elschakt ifrån ett angränsande rum. Kollade ett par gånger på bägge sidorna att var det verkade vara fritt för håltagning. Hann faktiskt fundera lite på varför det inte var några andra kablar genom väggen där, utan att ändå riktigt reflektera över det.
Men precis innan jag tänkte sätta borren i väggen så insåg jag plötsligt att väggen känns alldeles för tjock ... :x
Kollade lite till och mätte, ja självklart, det var ju ca en meter tjocklek, vad tusan kan det vara där. Efter lite konsultation av ritningar så insåg vi att de lodräta ventilationskanalerna för hela fastigheten löpte där inne, tur att jag inte borrade hål i dom då ...
Jag skulle ta hål för en canbus-kabel, in till ett elschakt ifrån ett angränsande rum. Kollade ett par gånger på bägge sidorna att var det verkade vara fritt för håltagning. Hann faktiskt fundera lite på varför det inte var några andra kablar genom väggen där, utan att ändå riktigt reflektera över det.
Men precis innan jag tänkte sätta borren i väggen så insåg jag plötsligt att väggen känns alldeles för tjock ... :x
Kollade lite till och mätte, ja självklart, det var ju ca en meter tjocklek, vad tusan kan det vara där. Efter lite konsultation av ritningar så insåg vi att de lodräta ventilationskanalerna för hela fastigheten löpte där inne, tur att jag inte borrade hål i dom då ...
Vi är nog rätt många i den klubben...
Jag skulle dra invändigt i en innervägg och borrade ut på andra sidan men såg inte det. Skulle sen använda dragfjädern för att fiska upp kabeln i ett dosborrat hål längre ner. Det var helt omöjligt att få tag i dragfjädern hur jag än höll på, efter ett tag noterade jag att det rasslade i hallen utanför när jag snodde runt med dragfjädern..... Tittar ut i hallen och ser dragfjädern sticka ut ur ett hål mitt i väggen....
Jag skulle dra invändigt i en innervägg och borrade ut på andra sidan men såg inte det. Skulle sen använda dragfjädern för att fiska upp kabeln i ett dosborrat hål längre ner. Det var helt omöjligt att få tag i dragfjädern hur jag än höll på, efter ett tag noterade jag att det rasslade i hallen utanför när jag snodde runt med dragfjädern..... Tittar ut i hallen och ser dragfjädern sticka ut ur ett hål mitt i väggen....
Inte direkt farlig men inte heller riktigt by The book. Ville så gärna få igång främre belysningen i garaget så då fick det bli en temporär lösning tills elektrikern har tid att kika förbi...
Om det ändå ska göras olagliga installationer, varför inte bara göra rätt direkt? Att koppla in en normal strömbrytare är precis lika enkelt, om inte enklare, än att koppla in det där. Bägge sätten är ändå olagliga.
Äh, fuskis. Du har ju bara vänt bilden. Jag trodde att du faktiskt hade flyttat brytaren.