Påstand (informatikk)

En forsikring , forsikring eller påstand ( latin / engelsk for uttalelse , påstand ) er en uttalelse om tilstanden til et dataprogram eller en elektronisk krets . Ved hjelp av forsikringer kan logiske feil i programmet eller mangler i den omkringliggende maskinvaren eller programvaren gjenkjennes og programmet avsluttes på en kontrollert måte. Når du utvikler elektroniske kretser, kan påstander brukes til å kontrollere samsvar med spesifikasjonen i verifiseringsfasen. Videre kan påstander gi informasjon om graden av testdekning under verifiseringen.

applikasjon

Ved å formulere en sikkerhet uttrykker utvikleren av et program sin tro på visse forhold i løpet av et program og gjør dem til en del av programmet . Han skiller denne troen fra de vanlige løpetidene og godtar disse forholdene som alltid sanne. Avvik fra dette blir ikke behandlet regelmessig slik at det store antallet mulige tilfeller ikke forhindrer løsningen av problemet, fordi det selvfølgelig kan skje i løpet av et program at 2 + 2 = 4 ikke gjelder en gang, f.eks. B. fordi variabler ble overskrevet av en programfeil i operativsystemet.

Dermed skiller forsikringene seg fra den klassiske feilkontrollen gjennom kontrollstrukturer eller unntak ( unntak ) som en feil som et mulig resultat inkluderer . I noen programmeringsspråk har forsikringer blitt innebygd i språknivået. De implementeres ofte som en spesiell unntaksform .

Feilhåndterere bør skrives for forventede feilforhold; Forsikringer for feilforhold som aldri skulle oppstå.

historie

Begrepet påstand ble introdusert av Robert Floyd i 1967 i sin artikkel Assigning Meanings to Programs . Han foreslo en metode for å bevise riktigheten av flytskjemaer ved å gi en sikkerhet for hvert element i flytskjemaet. Floyd ga regler som representasjoner kunne bestemmes av. Tony Hoare utviklet denne metoden videre til Hoare-beregningen for prosessuelle programmeringsspråk . I Hoare-logikken er en sikkerhet som går foran en instruksjon forutsetning (engelsk forutsetning ), en representasjon i henhold til en instruksjons- posttilstand (engelsk postcondition kalt). En forsikring som må oppfylles hver gang løkken kjøres, kalles en invariant .

Niklaus Wirth brukte forsikringer for å definere Pascals semantikk og foreslo at programmerere skrev kommentarer med påstander i programmene sine. Av denne grunn er kommentarer i Pascal omgitt av krøllete bukseseler {...}, en syntaks som Hoare brukte for påstander i sin beregning.

Ideen ble vedtatt i Borland Delphi og er innebygd som en systemfunksjon assert. Nøkkelordet er tilgjengelig på Java- programmeringsspråket fra versjon 1.4 assert.

Maskinvarebeskrivelsesspråkene VHDL og SystemVerilog brukes til å utvikle påstander om elektroniske kretser . PSL er et frittstående beskrivelsesspråk for påstander som støtter modeller i VHDL, Verilog og SystemC . Under verifiseringen registrerer simuleringsverktøyet hvor ofte påstanden ble utløst og hvor ofte forsikringen ble oppfylt eller brutt. Hvis påstanden ble utløst og forsikringen aldri ble brutt, anses kretsen å være bekreftet. Hvis påstanden aldri ble utløst under simuleringen, er det ikke tilstrekkelig testdekning, og verifiseringsmiljøet må utvides.

Programmeringspraksis

I programmeringsspråket C kan en forsikring brukes omtrent slik: 

#include <assert.h>
/// diese Funktion liefert die Länge eines nullterminierten Strings
/// falls der übergebene auf die Adresse NULL verweist, wird das
/// Programm kontrolliert abgebrochen. (strlen prüft das nicht selbst)
int strlenChecked(char* s) {
  assert(s != NULL);
  return strlen(s);
}

I dette eksemplet kan makroen brukes ved å inkludere overskriftsfilen assert.h . I tilfelle en feil, gir denne makroen en standardmelding der tilstanden som ikke er oppfylt er sitert og filnavnet og linjenummeret legges til. En slik melding kan se slik ut: assert

Assertion "s!=NULL" failed in file "C:\Projects\Sudoku\utils.c", line 9

Java kjenner begrepet forsikringer fra versjon 1.4. Her er imidlertid ikke programmet nødvendigvis komplett, men et såkalt unntak (engelsk unntak utløst), som kan behandles videre innenfor programmet.

Et enkelt eksempel på en påstand (her i Java-syntaks ) er 

int n = readInput();
n = n * n; //Quadrieren
assert n >= 0;

Med denne påstanden sier programmereren "Jeg er sikker på at etter dette punktet er n større enn eller lik null".

Bertrand Meyer behandlet ideen om forsikringer i programmeringsparadigmet Design by Contract og implementerte det på programmeringsspråket Eiffel . Forutsetninger er beskrevet av kreve klausuler, postconditions etter sikrer bestemmelser. Invarianter kan spesifiseres for klasser. Unntak reises også i Eiffel hvis en forsikring ikke blir oppfylt.

Relaterte teknikker

Påstander oppdager programfeil ved brukstid, dvs. bare når det er for sent. For å unngå meldinger om "interne feil" så langt det er mulig, blir det forsøkt å oppdage logiske feil i form av feil og advarsler ved kompileringstidspunktet (av kompilatoren ) ved passende formulering av kildeteksten . Logiske feil som ikke kan bli funnet på denne måten kan ofte avdekkes ved hjelp av modultester .

Omformulere kildekoden

Ved å redusere saksforskjellene til et minimum, kan noen feil ikke uttrykkes. Da er det heller ikke mulig som en logisk feil. 

// Kurvenrichtung
public enum TURN { LEFT_TURN, RIGHT_TURN }

// Methode liefert den Text zu einer Kurvenrichtung
public String getTurnText(TURN turn) {
  switch(turn) {
    case LEFT_TURN: return "Linkskurve";
    case RIGHT_TURN: return "Rechtskurve";
    default: assert false: "Es gibt nur Links- oder Rechtskurven"; // Kann nicht auftreten
  }
}

Forutsatt at det bare var to tilfeller (faktisk gjør de ofte), kunne vi bruke en enkel sannhetsverdi i stedet for en mer spesialisert koding: 

// Methode liefert den Text zu einer Kurvenrichtung
public String getTurnText(boolean isLeftTurn) {
  if (isLeftTurn) return "Linkskurve";
  return "Rechtskurve";
}

I mange tilfeller, som i dette eksemplet, gjør dette koden mindre eksplisitt og derfor mer uforståelig.

Forsikringer for kompileringstid

Mens påstandene beskrevet ovenfor blir sjekket når programmet kjører, er det i C ++ muligheten for å sjekke forhold når programmet kompileres av kompilatoren . Bare forhold som er kjent på kompileringstidspunktet kan kontrolleres, f.eks. B sizeof(int) == 4.. Hvis en test mislykkes, kan ikke programmet kompileres: 

#if sizeof(int) != 4
  #error "unerwartete int-Größe"
#endif

Tidligere var dette avhengig av funksjonaliteten til den respektive kompilatoren, og noen formuleringer brukte litt på å bli vant til: 

/// Die Korrektheit unserer Implementierung hängt davon ab,
/// dass ein int 4 Bytes groß ist. Falls dies nicht gilt,
/// bricht der Compiler mit der Meldung ab, dass
/// Arrays mindestens ein Element haben müssen:
void validIntSize(void) {
  int valid[sizeof(int)==4];
}

Med C11 og C ++ 11 ble nøkkelordene _Static_assert og static_assert (i tillegg implementert som en makro i C11) introdusert for å løse dette problemet : 

//in C als auch C++
void validIntSize(void) {
  static_assert(sizeof(int)==4,
    "implementation of validIntSize does not work with the int size of your compiler");
}

Forsikringer i modulprøver

Et område der forsikringer også spiller en rolle er modultester (inkludert en kjernekomponent i ekstrem programmering ). Hver gang du gjør endringer i kildekoden (f.eks. Refaktorer ), f.eks. B. for å integrere ytterligere funksjoner, blir det utført tester på underfunksjoner (moduler, f.eks. Funksjoner og prosedyrer, klasser) for å evaluere den kjente (ønsket) funksjonaliteten.

I motsetning til å hevde at hvis programmet mislykkes, avsluttes ikke hele programmet, bare testen anses å ha mislyktes, og ytterligere tester utføres for å finne så mange feil som mulig. Hvis alle testene kjører uten feil, bør det antas at ønsket funksjonalitet eksisterer.

Spesielt viktig er det faktum at modultester vanligvis ikke utføres i produktiv kode, men snarere på utviklingstidspunktet. Dette betyr at påstander skal sees på som motstykke i det ferdige programmet.

Spesielle teknikker for Microsoft kompilatorer

I tillegg til Assert brukes også Verify . Verify utfører alle utsagn som går inn i beregningen av tilstanden, uavhengig av om den ble kompilert med eller uten hensikt å feilsøke. Sjekken skjer bare i feilsøkingsversjonen, dvs. H. Også her kan et program mislykkes på en uklar måte hvis løftet ikke blir oppfylt. 

// die Variable anzahl wird immer erhöht
Verify(++anzahl>2);

Assert_Valid brukes til å teste objekter for deres gyldighet. Det er også den virtuelle metoden i baseklassen til objekthierarkiet AssertValid(). Metoden skal overskrives for hver spesifikke klasse for å teste de interne feltene i klassen for gyldighet. 

// Example for CObject::AssertValid.
void CAge::AssertValid() const
{
  CObject::AssertValid();
  ASSERT( m_years > 0 );
  ASSERT( m_years < 105 );
}

litteratur

  • Robert W. Floyd: Tilordne betydninger til programmer . I: Proceedings of Symposia in Applied Mathematics , bind 19, 1967, s. 19-32.

weblenker

Individuelle bevis

  1. ↑ Steve McConnell: Kode fullført. En praktisk håndbok for programvarekonstruksjon . Red.: Microsoft Press. 2. utgave. 2004, ISBN 978-0-7356-1967-8 (engelsk).