Prova:
{ true } [while(true, [skip])] { true } { true } [while(true, [skip])] { ( true and not true ) } { ( true and true ) } [skip] { true } { ( true and true ) } [skip] { ( true and true ) } ( ( true and true ) => true ) ( ( true and not true ) => true )Sentenças a serem provadas:
( ( true and not true ) => true ) ( ( true and true ) => true )Prova:
{ true } [while(true, [skip])] { true } { true } [while(true, [skip])] { ( true and not true ) } ( true => a ) { a } [while(true, [skip])] { ( true and not true ) } { a } [while(true, [skip])] { ( a and not true ) } { ( a and true ) } [skip] { a } { ( a and true ) } [skip] { ( a and true ) } ( ( a and true ) => a ) ( ( a and not true ) => ( true and not true ) ) ( ( true and not true ) => true )Sentenças a serem provadas:
( ( true and not true ) => true ) ( true => a ) ( ( a and not true ) => ( true and not true ) ) ( ( a and true ) => a )Prova:
{ true } [while(true, [skip])] { true } ( true => a ) { a } [while(true, [skip])] { true } { a } [while(true, [skip])] { ( a and not true ) } { ( a and true ) } [skip] { a } { ( a and true ) } [skip] { ( a and true ) } ( ( a and true ) => a ) ( ( a and not true ) => true )Sentenças a serem provadas:
( true => a ) ( ( a and not true ) => true ) ( ( a and true ) => a )