pulseverifier

Umiejętność integrująca FStar do weryfikacji plików Pulse (.fst) z dyrektywą #lang-pulse. Pozwala na debugowanie błędów dowodów logiki separacji i sprawdzanie poprawności zarządzania zasobami. Narzędzie interpretuje komunikaty błędów specyficzne dla Pulse, takie jak problemy z efektami ghost w kontekście obliczeń stanowych (stt) czy niezgodności typów erasowanych. Idealne dla programistów pracujących z formalną weryfikacją kodu.

1. Upewnij się, że masz zainstalowany FStar i dostęp do katalogu PULSE_HOME, który zwykle znajduje się obok głównego katalogu FStar. 2. Aby zweryfikować plik Pulse, uruchom fstar.exe z odpowiednimi ścieżkami include — minimalnie wymagana jest flaga --include /out/lib/pulse, na przykład: fstar.exe --include /out/lib/pulse Module.fst. 3. Jeśli pracujesz w repozytorium Pulse, możesz najpierw zbudować projekt poleceniem make -j4 w katalogu głównym, a następnie weryfikować konkretne pliki. 4. Gdy napotkasz błędy, zwróć uwagę na komunikaty specyficzne dla Pulse — najczęstsze to "Application of stateful computation cannot have ghost effect" (oznacza próbę wywołania funkcji stanowej wewnątrz kontekstu ghost) lub "Expected a term with non-informative (erased) type" (problem z typami erasowanymi). 5. Aby rozwiązać błędy logiki separacji, przeanalizuj, czy zmienne pochodzą z kontekstu ghost (bindowane z with x y z. _) — jeśli tak, zamiast nich używaj rzeczywistych struktur danych, a operacje stanowe wykonuj przed warunkami ghost. 6. Dla bardziej złożonych projektów weryfikuj najpierw interfejsy (.fsti), a następnie implementacje (.fst), dodając dodatkowe ścieżki include dla bibliotek Pulse (--include out/lib/pulse --include lib/pulse/lib).