Prova:
{ a } [while(true, [skip])] { a } { 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 ) => a )Sentenças a serem provadas:
( ( a and not true ) => a ) ( ( a and true ) => a )Prova:
{ a } [while(true, [skip])] { a } { a } [while(true, [skip])] { ( a and not true ) } ( a => true ) { true } [while(true, [skip])] { ( a and not 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 ) => ( a and not true ) ) ( ( a and not true ) => a )Sentenças a serem provadas:
( ( a and not true ) => a ) ( a => true ) ( ( true and not true ) => ( a and not true ) ) ( ( true and true ) => true )Prova:
{ a } [while(true, [skip])] { a } ( a => true ) { true } [while(true, [skip])] { a } { 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 ) => a )Sentenças a serem provadas:
( a => true ) ( ( true and not true ) => a ) ( ( true and true ) => true )