eGospodarka.pl
eGospodarka.pl poleca

eGospodarka.plGrupypl.comp.programmingFormal Methods Toolkit › Re: Formal Methods Toolkit
  • X-Received: by 2002:a1f:d142:: with SMTP id i63-v6mr3583211vkg.5.1525549505599; Sat,
    05 May 2018 12:45:05 -0700 (PDT)
    X-Received: by 2002:a1f:d142:: with SMTP id i63-v6mr3583211vkg.5.1525549505599; Sat,
    05 May 2018 12:45:05 -0700 (PDT)
    Path: news-archive.icm.edu.pl!news.icm.edu.pl!news.nask.pl!news.nask.org.pl!news.unit
    0.net!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!peer01.ams1!pee
    r.ams1.xlned.com!news.xlned.com!peer01.am4!peer.am4.highwinds-media.com!peer03.
    iad!feed-me.highwinds-media.com!news.highwinds-media.com!x25-v6no6633231qto.0!n
    ews-out.google.com!p41-v6ni1579qtp.1!nntp.google.com!x25-v6no6633224qto.0!postn
    ews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
    Newsgroups: pl.comp.programming
    Date: Sat, 5 May 2018 12:45:05 -0700 (PDT)
    In-Reply-To: <f...@g...com>
    Complaints-To: g...@g...com
    Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=213.108.152.51;
    posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
    NNTP-Posting-Host: 213.108.152.51
    References: <d...@g...com>
    <f...@g...com>
    User-Agent: G2/1.0
    MIME-Version: 1.0
    Message-ID: <6...@g...com>
    Subject: Re: Formal Methods Toolkit
    From: Maciej Sobczak <s...@g...com>
    Injection-Date: Sat, 05 May 2018 19:45:05 +0000
    Content-Type: text/plain; charset="UTF-8"
    Content-Transfer-Encoding: quoted-printable
    X-Received-Bytes: 3981
    X-Received-Body-CRC: 3291167577
    Xref: news-archive.icm.edu.pl pl.comp.programming:212439
    [ ukryj nagłówki ]

    > 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

Podziel się

Poleć ten post znajomemu poleć

Wydrukuj ten post drukuj

Najnowsze wątki z tej grupy


Najnowsze wątki

Szukaj w grupach

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: