Detalhes do Documento

Smart contracts are high-stakes software: their immutable, publicly accessible code may govern assets worth millions. This means that even minor defects can have severe consequences. Unit tests often miss edge cases. Although formal verification is the only route to full correctness, it demands substantial time and expertise. Property-based testing bridges this gap by exploring large input spaces and shrinking failures to minimal counterexamples. Used early, it filters defects and prioritises verification effort on code already validated by tests. Although Solidity benefits from a mature testing ecosystem, comparable support for other languages such as Daml remains limited. This dissertation addresses this gap by introducing Hypothesis2Daml, an open-source library that brings property-based testing to Damlby connecting Hypothesis withthe Daml JSON API. Hypothesis2Daml enables developers to specify invariants, pre/postconditions, and stateful workflows over realistic ledger interactions. It provides automatic input generation, shrinking to minimal counterexamples, party isolation per example, and request helpers that keep tests focused on properties rather than HTTP/JSON wiring. The approach is validated on a benchmark of eight contracts and twenty-seven properties that range from simple invariants to multi-step, role-sensitive workflows. All properties held under testing, with runs completing within practical time bounds, demonstrating that property-based testing is feasible and effective for Daml applications. A comparative evaluation situates Hypothesis2Daml among established tools and methods, highlighting strengths in usability and expressiveness, and acknowledging a throughput trade-off due to JSON-API transport overhead. Contributions include the Hypothesis2Daml library and a reusable benchmark with representative properties. Limitations concern transport overhead, ecosystem specificity, and dependence on developer-authored properties and generators. Future work targets automation, performance, andscope expansion. Together, these results establish a practical path for making property-based testing a routine part of building Daml applications.

Os contratos inteligentes são software de alto risco: o seu código imutável e publicamente acessível pode governar ativos no valor de milhões. Isto significa que mesmo defeitos menores podem ter consequências graves. Testes unitários muitas vezes não capturam casos-limite. Embora a verificação formal seja a única via para correção total, exige tempo e especialização substanciais. Testes baseados em propriedades superam essa lacuna ao explorar grandes espaços de entrada e reduzir falhas a contraexemplos mínimos. Usados cedo, filtram defeitos e priorizam o esforço de verificação no código já validado por testes. Embora Solidity beneficie de um ecossistema de testes maduro, suporte comparável para outras linguagens, como Daml, permanece limitado. Esta dissertação aborda essa lacuna ao introduzir Hypothesis2Daml, uma biblioteca pública que traz testes baseados em propriedades para Daml ao ligar o Hypothesis à API JSON do Daml. O Hypothesis2Daml permite aos programadores especificar invariantes, pré/pós-condições e fluxos com estado através de interações realistas com o ledger. Fornece geração automática de entradas, redução a contraexemplos mínimos, isolamento de parties por exemplo e auxiliares de pedido que mantêm os testes focados nas propriedades em vez da interligação HTTP/JSON. A abordagem é validada num benchmark de oito contratos e vinte e sete propriedades que variam de invariantes simples a fluxos multietapa sensíveis aos papeis específicos dos participantes. Todas as propriedades mantiveram-se sob teste, com execuções a concluírem dentro de limites de tempo práticos, demonstrando que testes baseados em propriedades são viáveis e eficazes para aplicações Daml. Uma avaliação comparativa situa o Hypothesis2Daml entre ferramentas e métodos estabelecidos, destacando pontos fortes de usabilidade e expressividade e reconhecendo um compromisso em termos de débito devido ao overhead de transporte da API JSON. As contribuições incluem a biblioteca Hypothesis2Daml e um benchmark reutilizável com propriedades representativas. As limitações centram-se no overhead de transporte, na especificidade do ecossistema e na dependência de propriedades e geradores definidos pelo programador. O trabalho futuro foca-se na automação, desempenho e expansão do âmbito. Em conjunto, estes resultados traçam um caminho prático para tornar os testes baseados em propriedades numa parte rotineira do desenvolvimento de aplicações Daml.