Retourner au contenu associé (dépêche : Sortie de Coq 8.5 bêta, un assistant de preuve formelle)
Posté par reno le 29 janvier 2015 à 14:02. En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 4.
Non PAS "à vouloir chercher la performance"!
En pseudo-assembleur, la version 'sophistiquée': xor Rx,Ry -> R1 and Rx,Ry -> R2 ushr R1,1 -> R1 add R1,R2 -> R1 4 instructions a décoder, 2 registres temporaires utilisés.
La version simple: sub Ry,Rx -> R1 ushr R1,1 -> R1 add Rx,R1 -> R1 3 instructions a décoder, 1 registre temporaire utilisé.
Après ça peut dépendre du CPU..
AltStyle によって変換されたページ (->オリジナル) / アドレス: モード: デフォルト 音声ブラウザ ルビ付き 配色反転 文字拡大 モバイル
[^] # Re: Idris
Posté par reno . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 4.
Non PAS "à vouloir chercher la performance"!
En pseudo-assembleur, la version 'sophistiquée':
xor Rx,Ry -> R1
and Rx,Ry -> R2
ushr R1,1 -> R1
add R1,R2 -> R1
4 instructions a décoder, 2 registres temporaires utilisés.
La version simple:
sub Ry,Rx -> R1
ushr R1,1 -> R1
add Rx,R1 -> R1
3 instructions a décoder, 1 registre temporaire utilisé.
Après ça peut dépendre du CPU..