Mostrando las entradas con la etiqueta análisis. Mostrar todas las entradas
Mostrando las entradas con la etiqueta análisis. Mostrar todas las entradas

martes, 27 de mayo de 2025

Las buenas maneras de las llamadas recursivas

The Power of 10 Rules (El poder de las 10 reglas) es una guía para código seguro creada en 2006 por Gerard J. Holzmann del Laboratorio de Software Fiable de la NASA/JPL.

Las reglas prohíben ciertas prácticas de codificación en C que dificultan la revisión o el análisis estático del código. Estas reglas son un complemento a las directrices MISRA C y se han incorporado en el mayor conjunto de estándares de codificación de JPL.

Las diez reglas

  1. Restrinja todo el código a construcciones de flujo de control muy simples. No utilice sentencias GOTO, construcciones set jmp o long jmp, ni recursividad directa o indirecta.
  2. Todos los bucles deben tener un límite superior fijo. Debe ser trivialmente posible para una herramienta de comprobación demostrar estáticamente que no se puede superar un límite superior preestablecido en el número de iteraciones de un bucle. Si el límite del bucle no puede demostrarse estáticamente, se considera que se ha infringido la norma.
  3. No utilice la asignación dinámica de memoria después de la inicialización.
  4. Ninguna función debe ser más larga de lo que se puede imprimir en una sola hoja de papel.
  5. Use un mínimo de dos aserciones en tiempo de ejecución por función. Las aserciones siempre deben estar libres de efectos secundarios y deben definirse como pruebas booleanas.
  6. El scope de los datos debe ser el más pequeño posible.
  7. Cada función de llamada debe comprobar los valores de retorno de función no vacíos, y la validez de los parámetros debe comprobarse dentro de cada función.
  8. El uso del preprocesador debe limitarse a los headers y definiciones de macros simples.
  9. El uso de punteros debe estar restringido a un nivel de des referencia. No se permiten punteros a funciones.
  10. Todo el código debe ser compilado, desde el primer día de desarrollo, con todas las advertencias del compilador habilitadas en la configuración más estricta del compilador. Todo el código debe ser comprobado diariamente con al menos un analizador estático de código fuente actualizado, y debe pasar los análisis con cero advertencias.

La primera regla prohíbe el uso de llamadas recursivas. Las normas de la NASA se centran en la robustez de sistemas de tiempo real que son siempre críticos y inaccesibles para mantenimiento: La recursión puede ser impredecible en sistemas embebidos o de tiempo real.El consumo de recursos no acotados (pila/stack), es crítico en hardware con memoria limitada (ej.: satélites, rovers). Dificultad para verificación formal (requerida en software de seguridad crítica).

Recursión Eficiente: Optimización del Compilador

Para hacer que la recursión sea eficiente y segura, los compiladores modernos aplican optimizaciones clave, pero requieren que el código cumpla ciertas condiciones.

Tail-Call Optimization (TCO)

El compilador reemplaza la llamada recursiva por un bucle (jump) si la recursión está en posición de cola (tail position), evitando crecimiento de la pila (stack). La llamada recursiva debe ser la última operación de la función. Compiladores como GCC/Clang la optimizan con -O2 o -O3.

Trampolining (para lenguajes sin TCO nativo)

Transforma la recursión en un bucle usando una estructura intermedia ("trampolín").

Memoization (Cache de Resultados)

Almacena resultados previos para evitar recalcular en recursión múltiple.

Conversión Manual a Iteración

Si el compilador no optimiza, transforma la recursión en un bucle manualmente.

Fuentes:

NASA JPL Institutional Coding Standard for the C Programming Language (2009).

DO-178C (Estándar para software aeronáutico).

Resumen y extractos en el repositorio técnico de la NASA: NASA Technical Reports Server (NTRS) (Busca "JPL C Coding Standard 2009")

Versión similar y pública (JPL Power of Ten Rules): NASA JPL Power of 10 Rules (Reglas clave resumidas).

DO-178C (Estándar para Software Aeronáutico) Documento oficial: Publicado por RTCA (Requiere compra): RTCA DO-178C (Costo aproximado: $200 USD).

Guías gratuitas relacionadas:

FAA Advisory Circular 20-115C (basado en DO-178C): FAA.gov (Busca "AC 20-115C"). 

martes, 20 de mayo de 2025

Automatización de Pruebas Matemáticas

Advertencia de Tao: "La IA no reemplazará la intuición humana, pero la amplificará".

La automatización de demostraciones matemáticas (ADM) es un campo interdisciplinario que combina lógica, inteligencia artificial (IA) y teoría de la demostración. Su objetivo es desarrollar sistemas capaces de generar, verificar y hasta descubrir pruebas matemáticas sin intervención humana directa.

Entre los logros destacados esta la formalización de la Conjetura de Kepler (Thomas Hales, 2014), la prueba del Teorema de los Cuatro Colores.

El desafíos clave es la complejidad computacional. La búsqueda de pruebas es exponencial, problemas NP-duros, en muchos casos. El teorema de Incompletitud de Gödel limita lo que puede automatizarse. Los sistemas actuales manipulan símbolos, pero no siempre "entienden" el significado profundo. Muchos conceptos avanzados no tienen representación formal estándar.

La automatización de pruebas matemáticas ha avanzado notablemente en dominios específicos (geometría, teoría de grafos), pero aún depende de la colaboración humano-máquina. Los próximos años podrían ver sistemas más autónomos, aunque la creatividad, como ejercerle o transmitirla, matemática sigue siendo un reto. Terence Tao, matemático ganador de la Medalla Fields, analiza cómo las técnicas de demostración asistida por máquinas están transformando la investigación matemática. Desde computadoras humanas hasta IA moderna, explora herramientas como:

  • Resolvedores SAT (para problemas de lógica).
  • Asistentes de prueba formal (Coq, Lean).
  • Algoritmos de aprendizaje automático (como AlphaGeometry).

Tao destaca el potencial de combinar estas tecnologías para:

  • Colaboración a gran escala (ej.: proyectos colaborativos como Mathlib en Lean).
  • Explorar problemas complejos que humanos solos no podrían abordar.
  • Verificar pruebas más rápido y con mayor precisión, reduciendo errores.
El 25% de las pruebas en arxiv.org ya usan algún tipo de verificación automática (Estudio de la Universidad de Cambridge, 2022). Terence Tao Tao propone 3 escenarios para el 2030:
  1. Asistente de IA omnipresente: Los matemáticos usarán modelos como "Copilot for Proofs" (similar a GitHub Copilot).
  2. Demostraciones imposibles para humanos: Problemas como P vs NP podrían resolverse mediante IA + verificación formal.
  3. Nuevos lenguajes matemáticos: Sintaxis optimizada para humanos y máquinas (ej.: MathLang).

domingo, 28 de febrero de 2016

Análisis de Sentimiento Social


Hay una nueva  a la que llamamos  de Sentimiento Social. Nuestro “Cerebro” del siglo 21 es factible gracias a la  en Nube; se alimenta de datos no estructurados -como posts en – que se generan cada vez más desde los  móviles, como una tendencia potencializada por lo social y que son analizados en tiempo real. Un sistema alimentado por las cuatro mega-tendencias actuales de mercado: Nube, Analítica, Movilidad y Social.

Sólo para darnos una idea de la  e impacto que estas mega-tendencias tienen en nuestras vidas y los negocios, considere lo siguiente: actualmente, 60 por ciento de las personas utilizan un  al menos una vez al día, mientras que sólo el 64 por ciento tiene acceso a  potable.

miércoles, 24 de febrero de 2016

ISO/IEC 27001


ISO/IEC 27001 es un estándar para la seguridad de la información (Information technology - Security techniques - Information security management systems - Requirements) aprobado y publicado como estándar internacional en octubre de 2005 por International Organization for Standardization y por la comisión International Electrotechnical Commission.

Especifica los requisitos necesarios para establecer, implantar, mantener y mejorar un sistema de gestión de la seguridad de la información (SGSI) según el conocido como “Ciclo de Deming”: PDCA - acrónimo de Plan, Do, Check, Act (Planificar, Hacer, Verificar, Actuar). Es consistente con las mejores prácticas descritas en ISO/IEC 27002, anteriormente conocida como ISO/IEC 17799, con orígenes en la norma BS 7799-2:2002, desarrollada por la entidad de normalización británica, la British Standards Institution(BSI).