El cálculo de números reales exactos es un campo de rápido crecimiento con aplicaciones que varían desde la depuración hasta la especificación de números a programas. Presentamos una especificación de los números reales representados como en listas cortas de dígitos con signo en Z. La precisión expresiva y la cercanía a la notación matemática teórica de conjuntos habituales nos dan una especificación limpia y legible que se puede implementar directamente. Una comparación con otros métodos formales se da junto con una prueba parcial de que el objeto que se está especificando es en realidad los números reales.

Le calcul exact des nombres réels est un domaine en croissance rapide avec des applications allant du débogage à la spécification du numérique au programme. Nous présentons une spécification des nombres réels représentés comme dans les listes nites de chiffres signés dans Z. Le p o w er expressif et la proximité de la notation mathématique théorique habituelle nous donne une spécification propre et lisible qui est en outre directement réalisable. Une comparaison avec d'autres méthodes formelles est donnée avec une preuve partielle que l'objet spécifié est en fait les nombres réels.

Exact real number computation is a fast growing eld with applications varying from debugging to speci cation of numerical to program.We present a speci cation of the real numbers represented as in nite lists of signed digits in Z.The expressive p o w er and closeness to usual set theoretical mathematical notation gives us a clean and readable speci cation which is further directly implementable.A comparison with other formal methods is given together with a partial proof that the object being speci ed is actually the real numbers.

يعد حساب العدد الحقيقي الدقيق مجالًا سريع النمو مع تطبيقات تتراوح من التصحيح إلى التحديد العددي إلى البرنامج. نقدم تحديدًا للأرقام الحقيقية الممثلة كما هو الحال في قوائم الأرقام الموقعة في Z. يمنحنا التدوين الرياضي النظري المعبر والقرب من التدوين الرياضي النظري المعتاد مواصفات نظيفة وقابلة للقراءة والتي يمكن تنفيذها بشكل مباشر. يتم تقديم المقارنة مع الطرق الرسمية الأخرى مع دليل جزئي على أن الكائن الذي يتم تحديده هو في الواقع الأرقام الحقيقية.