Wie um zu beweisen, eine SPARK.Text_IO Verfahren Voraussetzung

Question

halten wird ich SPARK.Text_IO aus dem spark_io Beispiel in SPARK Entdeckung 2017.

Mein Problem ist, dass ich viele der SPARK.Text_IO Verfahren eine Voraussetzung, dass ich Ich weiß nicht, wie ich anfangen soll zu beweisen, dass die Standardeingabe lesbar ist und wir nicht am Dateiende sind. Mein Versuch, wie im folgenden Code dargestellt, bestand darin, die Vorbedingung der SPARK.Text_IO-Prozedur (Get_Immediate in diesem Fall) der Voraussetzung der aufrufenden Prozedur hinzuzufügen und zu denken, dass dies dem Beweiser garantieren könnte, dass diese Voraussetzung wahr ist . Es hat nicht funktioniert. Hier ist ein Beispiel dafür, was ich spreche:

Test-spec:

with SPARK.Ada.Text_IO; use SPARK.Ada.Text_IO; 

package test with SPARK_Mode 
is 

    continue_messages_key : Character := ' '; 

    procedure User_Wait_For_Continue_Messages_Key 
    with Global => (In_Out => Standard_Input, 
        Input => continue_messages_key), 
     Pre => Is_Readable (Standard_Input) and then 
        not End_Of_File; 

end test; 

Prüfkörper:

pragma SPARK_Mode(On); 

package body test is 

    procedure User_Wait_For_Continue_Messages_Key 
    is 
     IR : Immediate_Result; 
     Avail : Boolean; 
    begin 
     loop 
     Get_Immediate(IR, Avail); 
     if Avail then 
      if IR.Status = Success then 
       if IR.Available = True then 
        if IR.Item = continue_messages_key then 
        return; 
        end if; 
       end if; 
      end if; 
     end if; 
     end loop; 
    end User_Wait_For_Continue_Messages_Key; 

end test; 

Der Fehler der Prover ist auf der Get_Immediate Linie gibt „Medium: Voraussetzung könnte fail "Der Prototyp und der Vertrag des Get_Immediate-Verfahrens sind unten:

Wie? Sie beweisen SPARK, dass Standard_Input lesbar ist und dass es nicht das Ende der Datei ist?

Answer 1

Lassen Sie mich damit beginnen zu sagen, ich habe SPARK seit den Tagen der besonderen Kommentare nicht verwendet, so dass meine Antwort möglicherweise nicht aktuelle Verwendung widerspiegelt.

Eine Möglichkeit, SPARK zu betrachten, ist, dass Sie über alles nachdenken, was Ihr Programm möglicherweise vorfindet. Was sollte Ihr Programm tun, wenn die Vorbedingung False ist? Du musst zeigen, dass du diese Möglichkeit in Betracht gezogen hast.

der Annahme, dass alle SPARK.Ada.Text_IO Operationen auf Standard_Input haben eine Nachbedingung einschließlich Is_Readable (Standard_Input) als Get_Immediate ist, dann sollte es genügen, so etwas wie

pragma Assert (Is_Readable (Standard_Input)); 

am Anfang des Programms zu setzen und fügen Sie diese der Nachbedingung Ihrer Prozedur (und alle anderen Unterprogramme, die Sie lesen Standard_Input). Dann sollten Sie sicher sein, dass dieser Teil der Vorbedingung für Ihr gesamtes Programm gilt. (Die Bestätigung ist möglicherweise nicht erforderlich, wenn SPARK zunächst garantiert, dass Standard_Input lesbar ist.)

not End_Of_File ist ein bisschen komplizierter. Es ist möglich, dass es zumindest auf einigen Plattformen falsch ist. Linux behandelt zum Beispiel Strg-D als EOF, wenn es als erstes in einer Zeile eingegeben wird. Es gibt auch Fälle, in denen Sie von einer Pipe oder einer Eingabeumleitung lesen. Ihre Prozedur ruft möglicherweise Get_Immediate auf, wenn End_Of_File True ist, wenn der Benutzer EOF während der Schleife eingibt, also ist es nicht überraschend, dass SPARK nichts anderes beweisen kann. Wahrscheinlich müssen Sie vor der Voraussetzung des Verfahrens um diesen Teil zu nehmen und Ihren Körper etwas ändern wie

All_Chars : loop 
    if not End_Of_File then 
     Get_Immediate (IR, Avail); 

     exit All_Chars when Avail    and then 
          IR.Status = Success and then 
          IR.Available  and then 
          IR.Item = Continue_Messages_Key; 
    end if; 
end loop All_Chars; 

Dann werden Sie sicher sein, die Voraussetzung für Get_Immediate zufrieden ist und haben das scheinbar gewünschte Verhalten (Endlosschleife), wenn End_Of_File wird True (vorausgesetzt, dass ein IR-Feld in diesem Fall einen Ihrer Checks nicht besteht).

Es gibt einige verwirrende Dinge über Ihren Code. Erstens ist die globale Variable. Globale Variablen sind die Wurzel allen Übels oder garantieren zumindest unlesbaren Code. Dann gibt es die Besonderheit des Verfahrens.Wäre nicht etwas allgemeiner, wie

procedure Wait_For_Key (Key : in Character); 

genauso einfach zu schreiben und zu beweisen, und nützlicher? Dann gibt es die Zeichenfolge von verschachtelten if-Anweisungen, die ich schwieriger zu lesen als die entsprechenden Bedingungen mit and then verbunden sind. Schließlich wird ein Boolescher Wert mit True verglichen. Da "=" Boolean zurückgibt, bedeutet das nicht, dass ein Boolescher Wert benötigt wird, der sich bereits auf der linken Seite von "=" befindet?

Vielleicht bedeutet dies, dass das Ergebnis von "=" auch mit True verglichen werden muss. Dann muss das Ergebnis dieses "=" auch mit True verglichen werden. Dies könnte besser sein, da es sicherstellt, dass derjenige, der dies schreibt, niemals fertig wird.