On Mon, Feb 17, 2003 at 10:03:21AM +, Lutz Donnerhacke wrote:
[...]
> > Weil das keine komplizierten Eigenschaften sind. Halbwegs kompliziert
> > wäre z.B. die Implementation eines Filesystems darauf zu testen, ob
> > die Datenstrukturen auf der Platte immer konsistent bleiben.
>
> Ich halte
* Martin Uecker wrote:
> Die Frage ist doch, was für Eigenschaften man verifiziert, nicht in
> welchen System. Deine Beispiele (Division durch 0, Bereichsüberschreitungen)
> sind normalerweise Eigenschaften, die sehr leicht zu beweisen sind.
Dann haben wir aneinander vorbei geschrieben. Mir ging e
* Martin Uecker wrote:
>>> Aber selbst dann wird man für komplexe Programmsysteme, die in
>>> imperativen Sprachen geschrieben sind, niemals irgenwelche
>>> komplizierten Eigenschaften beweisen können.
>>
>> Beweis durch Behauptung? Warum klappt das dann in den o.g. Beispielen?
>
> Weil das keine
On Fri, Feb 14, 2003 at 04:49:43PM +, Lutz Donnerhacke wrote:
[...]
> > Aber selbst dann wird man für komplexe Programmsysteme, die in
> > imperativen Sprachen geschrieben sind, niemals irgenwelche komplizierten
> > Eigenschaften beweisen können.
>
> Beweis durch Behauptung? Warum klappt das
Lutz Donnerhacke <[EMAIL PROTECTED]> writes:
> Es ist Fun, zuverlässige Software zu schreiben. Es ist noch mehr
> Fun, bewiesenermaßen partiell korrekte Software zu schreiben (das
> leistet SPARK nur, wenn man formale Specs baut, z.B. in Z)
Wenn Du meinst. Das Problem ist, daß ich mit SPARK nicht
On Thu, Feb 13, 2003 at 04:55:57PM +, Lutz Donnerhacke wrote:
> > Eigentlich nie, oder kennst Du ein Beispiel?
>
> Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik.
Mißverständnis. Ich wollte eigentlich wissen, ob es ein
Open Source-Projekt gibt, das sowas macht.
> > Und selb
* Martin Uecker wrote:
> On Thu, Feb 13, 2003 at 04:55:57PM +, Lutz Donnerhacke wrote:
>> > Eigentlich nie, oder kennst Du ein Beispiel?
>>
>> Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik.
>
> Mißverständnis. Ich wollte eigentlich wissen, ob es ein
> Open Source-Projekt gibt,
* Dietz Proepper wrote:
> Zusammengefasst - es sieht den letzten 50 magic bullets leider recht ähnlich.
Wenn Du meinst. Ich habe keine Zeit für Bauchpinselung von Skeptikern.
> Grüß' Gödel von mir,
Gödel wird nicht touchiert, aber das wirst Du irgendwann auch von selbst
verstehen.
Lutz Donnerhacke:
[Verifikation]
> > Das Ganze war auch schon von 15 Jahren möglich und wurde (zumindest auf
> > dem Papier) auch gemacht. Leider kann man einfach zeigen das "alle"
> > automatisch nicht geht. Schon sind wir wieder bei harter Handarbeit,
> > diese ist fehlerträchtig und keine prinzi
* Martin Uecker wrote:
> On Wed, Feb 12, 2003 at 09:56:41PM +, Lutz Donnerhacke wrote:
>> > Letzteres ist auch bei abstrakter ("hochsprachlicher") Formulierung
>> > aufwendig bis unmöglich, ersteres wird nicht wesentlich aufwendiger.
>>
>> Eine formale Verifizierung der Abwesenheit von Fehlerkl
On Wed, Feb 12, 2003 at 09:56:41PM +, Lutz Donnerhacke wrote:
[...]
> > Letzteres ist auch bei abstrakter ("hochsprachlicher") Formulierung
> > aufwendig bis unmöglich, ersteres wird nicht wesentlich aufwendiger.
>
> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
>
Hi Lutz,
On Wed, 12 Feb 2003, Lutz Donnerhacke wrote:
> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
> Abwesenheit aller Laufzeitfehler) ist heute schon möglich und wird gemacht.
Ehrlich, gibt's da _Praktikables_? Kannst Du mich mal auf Anschauens- und
Lesenswertes,
Lutz Donnerhacke:
> * Dietz Proepper wrote:
> > Anderson übersieht eine Kleinigkeit - es gibt im engeren Sinn sowas wie
> > closed source nicht. Es ist natürlich wesentlich aufwendiger, anhand
> > eines Compilats Einsichten zu gewinnen - aber keinesfalls unmöglich.
>
> Das ist Ross klar. Er hat nur
* Dietz Proepper wrote:
>> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
>> Abwesenheit aller Laufzeitfehler) ist heute schon möglich und wird gemacht.
>
> Das Ganze war auch schon von 15 Jahren möglich und wurde (zumindest auf
> dem Papier) auch gemacht. Leider kann man
* Dietz Proepper wrote:
> Anderson übersieht eine Kleinigkeit - es gibt im engeren Sinn sowas wie
> closed source nicht. Es ist natürlich wesentlich aufwendiger, anhand
> eines Compilats Einsichten zu gewinnen - aber keinesfalls unmöglich.
Das ist Ross klar. Er hat nur den Unterschied verlernt. :-
Axel H Horns:
> http://www.theregister.co.uk/content/55/29294.html
>
> -- CUT ---
>
> Open and closed security are roughly equivalent
>
> By John Leyden
>
> Posted: 12/02/2003 at 09:48 GMT
>
> Open and closed approaches to security are basical
http://www.theregister.co.uk/content/55/29294.html
-- CUT ---
Open and closed security are roughly equivalent
By John Leyden
Posted: 12/02/2003 at 09:48 GMT
Open and closed approaches to security are basically equivalent, with
open
17 matches
Mail list logo
