eGospodarka.pl
eGospodarka.pl poleca

eGospodarka.plGrupypl.comp.programmingjedno proste pytanieRe: jedno proste pytanie
  • Path: news-archive.icm.edu.pl!news.rmf.pl!nf1.ipartners.pl!ipartners.pl!news.nask.pl!
    news.nask.org.pl!newsfeed00.sul.t-online.de!t-online.de!border2.nntp.dca.gigane
    ws.com!nntp.giganews.com!postnews.google.com!w30g2000yqw.googlegroups.com!not-f
    or-mail
    From: Maciej Sobczak <s...@g...com>
    Newsgroups: pl.comp.programming
    Subject: Re: jedno proste pytanie
    Date: Tue, 17 Aug 2010 06:22:41 -0700 (PDT)
    Organization: http://groups.google.com
    Lines: 54
    Message-ID: <1...@w...googlegroups.com>
    References: <i3uu1t$lc5$1@inews.gazeta.pl> <4...@n...onet.pl>
    NNTP-Posting-Host: 137.138.182.236
    Mime-Version: 1.0
    Content-Type: text/plain; charset=ISO-8859-2
    Content-Transfer-Encoding: quoted-printable
    X-Trace: posting.google.com 1282051361 16031 127.0.0.1 (17 Aug 2010 13:22:41 GMT)
    X-Complaints-To: g...@g...com
    NNTP-Posting-Date: Tue, 17 Aug 2010 13:22:41 +0000 (UTC)
    Complaints-To: g...@g...com
    Injection-Info: w30g2000yqw.googlegroups.com; posting-host=137.138.182.236;
    posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
    User-Agent: G2/1.0
    X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.2.6)
    Gecko/20100625 Firefox/3.6.6,gzip(gfe)
    Xref: news-archive.icm.edu.pl pl.comp.programming:186563
    [ ukryj nagłówki ]

    On 17 Sie, 13:01, j...@p...onet.pl wrote:

    > Każdy student informatyki wie, że:
    > poprawność = częściowa poprawność + własność stopu + określoność obliczeń
    > gdzie częsciowa poprawność = zgodność z formalną specyfikacją

    To zależy, gdzie student studiował.

    http://en.wikipedia.org/wiki/Partial_correctness

    Częściowa poprawność oznacza, że JEŚLI program w ogóle da jakieś
    wyniki, to będą one poprawne. W szczególności częściowa poprawność nie
    chroni przed zapętleniem się.

    > No właśnie o to chodzi, że testami się tej pewności nie osiągnie, natomiast są
    > metody formalne, np. logika Hoare'a które taką pewność dają. Problem, w tym, że
    > są to metody pracochłonne i - przy bardziej skomplikowanych programach - trudne
    > matematycznie. Stąd całe moje pytanie: czy programiści wykorzystują je w
    > praktyce.

    Tak. Jednym z ciekawszych rozwiązań w tym zakresie jest SPARK:

    http://en.wikipedia.org/wiki/SPARK

    Jest ciekawy dlatego, że będąc podzbiorem znanego już języka
    imperatywnego jest też od razu kompilowalny do kodu wynikowego. To nie
    są jakieś obrazki czy inne matematyczne robaczki, tylko żywy kod z
    dodatkową specyfikacją nt. przepływu informacji czy pre/post-
    conditions. Weryfikuje się taki kod odpowiednimi narzędziami a potem
    wrzuca do normalnego kompilatora i działa. Sporo tym można zrobić i
    nawet się tego używa w praktyce a ponieważ kompletny zbiór narzędzi
    jest dostępny za friko, to jest to też dobra platforma dla samouków.

    > Oczywiście są sytuacje kiedy dowód formalny poprawności jest bardzo
    > pożądany, np. gdy od poprawności programu zależy ludzkie życie.

    Nadal pozostaje pytanie o poprawność specyfikacji. Można spokojnie
    udowodnić poprawność źle wyspecyfikowanego programu - program będzie
    idealnie robił nie to, co trzeba. Niestety zawsze gdzieś będzie
    miejsce na czynnik ludzki jako najsłabsze ogniwo.

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

Podziel się

Poleć ten post znajomemu poleć

Wydrukuj ten post drukuj


Następne wpisy z tego wątku

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: