Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

Manual de Referencia: motoko

Motoko — Verificador de Encapsulamiento Estricto, Opacidad de Structs e Invariantes de TDA

Motoko — Verificador de Encapsulamiento Estricto, Opacidad de Structs e Invariantes de TDA


1. Propósito y Filosofía Pedagógica

La herramienta motoko forma parte del ecosistema oficial de software de la cátedra. Su diseño sigue principios pedagógicos rigurosos:

  1. Evidencia Técnica Directa: Todo diagnóstico se fundamenta en la norma ISO C (C11/C23), en el modelo de memoria del sistema o en convenciones arquitectónicas formales.

  2. Acción Correctiva Concreta: Cada advertencia incluye la prescripción técnica inmediata para resolver el defecto sin recurrir a conjeturas.

  3. Autonomía del Estudiante: Facilita la autoevaluación local antes de la entrega final del trabajo práctico.

  4. Objetividad Docente: Estandariza la corrección automática removiendo discrepancias subjetivas en la evaluación.


2. Instalación y Verificación del Entorno

2.1 Requisitos Previos del Sistema

Instalá los paquetes del sistema requeridos según tu distribución o entorno:

Ubuntu / Debian
Arch Linux / Manjaro
Fedora / RHEL
macOS (Homebrew)
Windows (MSYS2 / WSL2)

sudo apt update && sudo apt install -y
build-essential
gcc
gdb
valgrind
clang-format
libclang-dev
bubblewrap
typst
graphviz
python3-pip
python3-venv


2.2 Métodos de Instalación de motoko

Podés instalar motoko mediante cualquiera de los siguientes métodos estándar:

uv tool (Recomendado)
pip / venv
pipx

Instalación aislada de alta velocidad con uv

uv tool install . --editable

O instalar todo el ecosistema de herramientas de la cátedra en lote:

source ./install_tools.sh


2.3 Autocompletado en la Shell

La interfaz CLI de motoko cuenta con autocompletado nativo para comandos, flags y archivos. Para configurarlo permanentemente en tu shell:

# Configuración automática en Bash / Zsh / Fish
motoko --install-completion

# Para cargar el autocompletado en la sesión actual de inmediato:
source ./install_tools.sh

2.4 Verificación del Entorno con doctor

Toda herramienta del ecosistema cuenta con el subcomando unificado doctor. Ejecutalo para auditar el estado del entorno:

motoko doctor
Comprobaciones Ejecutadas por el Diagnóstico:
Matriz de Resolución de Problemas:
Síntoma / Alerta de doctorCausa RaízAcción Correctiva
❌ gcc / clang no encontradoToolchain C faltanteInstalá build-essential o base-devel.
❌ bwrap permisos insuficientesUser namespaces desactivadosHabilitá sysctl kernel.unprivileged_userns_clone=1.
❌ typst no disponibleMotor de PDF faltanteDescargá Typst vía cargo install typst-cli o gestor de paquetes.
❌ gdb no respondeGDB sin interfaz MI/PythonReinstalá gdb completo desde el repositorio oficial.

3. Referencia Completa de Comandos CLI

A continuación se detallan los subcomandos principales disponibles en motoko:

Sintaxis del ComandoDescripción y Efecto
motoko check include/ src/Verifica que los clientes no rompan la encapsulación de los TDAs.
motoko opacify include/lista.hConvierte una struct pública en un tipo opaco forward-declared.
motoko invariants src/tda_pila.cAudita que las funciones públicas preserven los invariantes del TDA.
motoko doctorComprueba el analizador AST de C.

4. Tutorial Paso a Paso con Ejemplos Reales

Caso de Estudio

Considerá el siguiente fragmento de código representativo:

1
2
3
4
5
6
7
8
9
10
11
// include/lista.h (Encapsulado estricto con Motoko)
typedef struct lista t_lista; // Tipo opaco: cliente NO ve los campos

t_lista* lista_crear(void);
void lista_destruir(t_lista *lista);

// src/lista.c (Implementación privada)
struct lista {
    struct nodo *primero;
    size_t cantidad;
};

Ejecución de la Herramienta

Ejecutá el análisis desde tu terminal:

motoko check include/ src/

Salida Obtenida en Consola

[!] MOTOKO ENCAPSULATION VIOLATION en src/main.c:15:10:
    Acceso prohibido al miembro privado 'lista->cantidad'.
    Los campos internos de 'struct lista' son opacos para el código cliente.
    Sugerencia: Utilizá la función pública 'size_t lista_cantidad(const t_lista *l);'.

5. Ejercicios Prácticos y Desafíos

Practicá el uso avanzado de motoko resolviendo los siguientes ejercicios:


6. Integración en el Flujo de Trabajo y Makefile

Para incorporar motoko de forma automática a tu flujo de desarrollo, agregá la siguiente regla en el Makefile de tu proyecto:

check-motoko:
	@echo "=== Ejecutando verificación con motoko ==="
	motoko check src/ include/

.PHONY: check-motoko

Ejecutá make check-motoko antes de cada commit para mantener que tu código conserve el estado de aprobación.


7. Arquitectura Interna y Mecanismo Técnico

La herramienta motoko implementa un motor de alta precisión basado en:


8. Integración y Conexión con el Ecosistema

Diagrama de Flujo e Interoperabilidad

Matriz de Intercambio de Datos

CanalHerramientas ConectadasTipo de Datos Transferidos
Entradas (Inputs)- Código cliente (.c) y headers públicos (.h) de TDAsCódigo fuente, AST, binarios, testcases, contratos
Salidas (Outputs)- ripley (reglas 0x2000h de modularidad)

Pipeline de Integración Recomendado

Podés encadenar motoko con otras herramientas del ecosistema en una única línea de comando:

# Pipeline de integración típico
motoko check include/ src/ && ripley check src/

9. Extensión, Desarrollo de Plugins y API Python

Para crear tus propias reglas, conectores de evaluación o integrar motoko programáticamente en pipelines de CI/CD: