source language intermediate language passive command verification condition Tr[ x := E ]=x := E Tr[ assert E ]=assert E Tr[ S;T ]=Tr[ S ] ; Tr[ T ] T
{"Image DocumentName": "Tr[ x := E ] = x := E Tr[ assert E ] = assert E", "Image ImageDescription": "source language. intermediate language. passive command. verification condition. Tr[ x := E ] = x := E. Tr[ assert E ] = assert E. Tr[ S;T ] = Tr[ S ] ; Tr[ T ] Tr[ if E then S else T end ] = ( assume E ; Tr[ S ] [] assume \u00acE ; Tr[ T ] ) Tr[ while E do S end ] = while   do assume E ; Tr[ S ] end ; ( assume E ; Tr[ S ] ; assume false [] assume \u00acE ) x :=   ; assume J.", "Image XResolution": "37", "Image YResolution": "37", "Image ResolutionUnit": "Pixels/Centimeter", "Image Software": "SlidePlayer", "Image YCbCrPositioning": "Centered"}