eGospodarka.pl

eGospodarka.plGrupypl.comp.programming › Formal Methods Toolkit
Ilość wypowiedzi w tym wątku: 5

  • 1. Data: 2018-04-23 08:46:21
    Temat: Formal Methods Toolkit
    Od: Maciej Sobczak <s...@g...com>

    Z przyjemnością informuję o dostępności nowego narzędzia:

    http://inspirel.com/fmt/

    FMT jest pakietem rozszerzeń dla programu Mathematica, pozwalającym na tworzenie
    modeli, analizę, wizualizaję, weryfikację i generację kodu dla Ady, C i C++.

    Kilka zrzutów ekranu pokazuje próbkę możliwości:

    http://inspirel.com/fmt/gallery.html

    FMT jest narzędziem open-source.


    Chętnie odpowiem na pytania.

    --
    Maciej Sobczak * http://www.inspirel.com


  • 2. Data: 2018-04-23 20:58:41
    Temat: Re: Formal Methods Toolkit
    Od: denat 'POPIS/EU <N...@g...pl>

    uwaga atak:
    rozpoznaje dźwięki?


  • 3. Data: 2018-04-24 13:30:40
    Temat: Re: Formal Methods Toolkit
    Od: Roman Tyczka <n...@b...no>

    On Mon, 23 Apr 2018 20:58:41 +0200, denat 'POPIS/EU wrote:

    > uwaga atak:
    > rozpoznaje dźwięki?

    https://www.youtube.com/watch?v=j9ejj_fD-P0

    --
    pozdrawiam
    Roman Tyczka


  • 4. Data: 2018-05-05 09:12:11
    Temat: Re: Formal Methods Toolkit
    Od: m...@k...org

    On Monday, April 23, 2018 at 7:46:23 AM UTC+1, Maciej Sobczak wrote:
    > Z przyjemnością informuję o dostępności nowego narzędzia:
    >
    > http://inspirel.com/fmt/
    >
    > FMT jest pakietem rozszerzeń dla programu Mathematica, pozwalającym na tworzenie
    modeli, analizę, wizualizaję, weryfikację i generację kodu dla Ady, C i C++.
    >
    > Kilka zrzutów ekranu pokazuje próbkę możliwości:
    >
    > http://inspirel.com/fmt/gallery.html
    >
    > FMT jest narzędziem open-source.
    >
    >
    > Chętnie odpowiem na pytania.
    >

    Czy to jest po prostu nowy język programowania pozwalający na jakąś formę dowodzenia
    poprawności?
    Jak on się ma do - coraz popularniejszych, choć wciąż niszowych - języków typu Coq,
    Agda, Idris opartych o dependent types?

    --
    Michal


  • 5. Data: 2018-05-05 21:45:05
    Temat: Re: Formal Methods Toolkit
    Od: Maciej Sobczak <s...@g...com>

    > Czy to jest po prostu nowy język programowania

    Sprawa jest bardziej złożona. Nie jest to zupełnie nowy język, bo wykorzystuje
    gramatykę języka Wolfram. Tzn. każda konstrukcja w FMT jest poprawnym wyrażeniem
    języka Wolfram, choć z nowym znaczeniem wynikającym z tego, jak dane wyrażenie jest
    dalej obrabiane. Nie jest to też po prostu język programowania, bo nacisk jest na
    modelowanie systemu na poziomie wymagań niskopoziomowych. W swoim rdzeniu taki model
    faktycznie wygląda jak imperatywny kod albo pseudokod, ale nie jest to ograniczenie i
    być może język zostanie rozwinięty w stronę bardziej wysokopoziomowych konstrukcji,
    niekoniecznie opartych na kodzie w sensie tekstowego formatu. Ostatecznie kod
    programu jest generowany na podstawie modelu.

    > pozwalający na jakąś formę dowodzenia poprawności?

    Tak, ideą jest statyczne dowodzenie różnych wybranych cech modelu.

    > Jak on się ma do - coraz popularniejszych, choć wciąż niszowych - języków typu Coq,
    Agda, Idris opartych o dependent types?

    1. Podstawowym założeniem w FMT jest zdolność do wygenerowania kodu, który w ogóle
    nie potrzebuje run-time'u, co ma ułatwić wdrożenie w *prawdziwych* systemach
    krytycznych, czyli takich, które podlegają narzuconym z góry przemysłowym standardom.
    Czyli żadnej pamięci dynamicznej (nawet niejawnej), itp. Celem jest też generacja
    kodu w Adzie lub w C(++), które są standardowymi językami wykorzystywanymi w
    przemyśle - po to, żeby można było taki wygenerowany kod użyć w jakimś regularnym i
    uznanym obecnie procesie produkcyjnym. Inaczej mówiąc, można użyć FMT w obecnym
    procesie, bez technicznych rewolucji, bo z punktu widzenia obecnych procesów jest to
    tzw. Model-Based Design z generatorem kodu, czyli coś, co z powodzeniem uprawia się
    od dawna (patrz np. Simulink, SCADE, itp.).
    O ile zgaduję, takie założenia nie były priorytetem w tych językach, które
    wymieniłeś.

    2. Co to jest "dependent types"?
    W FMT system typów to ścisły podzbiór tego, co można osiągnąć w C albo w Adzie. Ma to
    związek z założeniami powyżej.

    --
    Maciej Sobczak * http://www.inspirel.com

strony : [ 1 ]



Szukaj w grupach

Szukaj w grupach

REKLAMA

Eksperci egospodarka.pl

1 1 1

Wpisz nazwę miasta, dla którego chcesz znaleźć jednostkę ZUS.

Wzory dokumentów

Bezpłatne wzory dokumentów i formularzy.
Wyszukaj i pobierz za darmo:

Strona korzysta z plików cookies w celu realizacji usług i zgodnie z Polityką Prywatności. Możesz określić warunki przechowywania lub dostępu do plików cookies w Twojej przeglądarce.