Analisis dan Verifikasi Correctness Algoritma Perhitungan Total Pembayaran pada Sistem Checkout E-Commerce
Keywords:
correctness algoritma, verifikasi formal, e-commerce, checkout, partial correctness, loop invariantAbstract
Keandalan algoritma merupakan aspek krusial dalam pengembangan sistem komputasi, khususnya pada aplikasi transaksi digital seperti e-commerce. Penelitian ini bertujuan menganalisis dan memverifikasi correctness algoritma perhitungan total pembayaran pada sistem checkout e-commerce menggunakan pendekatan verifikasi formal. Implementasi dilakukan menggunakan bahasa pemrograman Python dan diuji menggunakan data transaksi nyata dari beberapa struk pembelian e-commerce. Analisis correctness meliputi pembuktian precondition, postcondition, loop invariant, partial correctness, dan termination. Hasil pengujian menunjukkan bahwa nilai total pembayaran yang dihasilkan algoritma sesuai dengan data transaksi pada seluruh kasus yang diuji tanpa ditemukan perbedaan. Keberadaan loop invariant pada proses perhitungan subtotal memastikan konsistensi hasil pada setiap iterasi. Penelitian ini memberikan kontribusi berupa pendekatan sistematis untuk memverifikasi kebenaran algoritma transaksi digital sebagai dasar pengembangan sistem pembayaran yang lebih andal dan terpercaya.
References
A. M. Abdulaziz and K. Mehlhorn, “A formal correctness proof of Edmonds’ blossom shrinking algorithm,” Journal of Automated Reasoning, vol. 70, pp. 1–37, 2026.
A. Bezza, R. Benaboud, T.-M. Maarouk, and R. Ameur-Boulifa, “Formal verification of the correctness and soundness of a Pomset-to-LTS transformation algorithm,” Journal of Communications Software and Systems, vol. 21, no. 4, 2025.
A. Jaszczak, “Partial correctness of an algorithm computing Lucas sequences,” Formalized Mathematics, vol. 28, pp. 280–286, 2020.
A. Muhammad et al., “Formal verification of transcompiled mobile applications using first-order logic,” Technologies, vol. 13, pp. 1–19, 2025.
C. Pilatte, “Unconditional correctness of recent quantum algorithms for factoring and computing discrete logarithms,” Forum of Mathematics, pp. 1–22, 2026.
C. Yang, S. Wu, and Q. Cao, “A formal framework for naturally specifying and verifying sequential algorithms,” arXiv, 2025.
F. Stoica and L. F. Stoica, “Formal verification of business constraints in workflow-based applications,” Information, vol. 15, no. 12, 2024.
G. Ernst, “A complete approach to loop verification with invariants and summaries,” arXiv, 2021.
H. N. Nguyen and A. Rakio, “Formal modelling and verification of probabilistic resource bounded agents,” Journal of Logic, Language and Information, vol. 32, pp. 829–859, 2023.
H. Wang and L. Song, “Study of Isabelle/HOL on formal algorithm analysis and code generation,” IEEE Access, vol. 9, pp. 25002–25013, 2021.
K. S. Namjoshi and L. D. Zuck, “Program correctness through self-certification,” Communications of the ACM, vol. 68, no. 2, pp. 74–83, 2025.
L. Cheung, A. Moffat, and C. Rizkallah, “Formally verified suffix array construction,” Journal of Automated Reasoning, vol. 69, pp. 1–38, 2025.
L. Nigro and F. Cicirelli, “Correctness verification of mutual exclusion algorithms by model checking,” Preprints.org, 2024.
L. Nigro and F. Cicirelli, “Formal verification of mutual exclusion algorithms in anonymous memory,” Applied Computing and Intelligence, vol. 5, pp. 236–263, 2025.
L. Nigro and F. Cicirelli, “Proving properties of Dekker's algorithm for mutual exclusion of N processes,” Algorithms, vol. 18, no. 4, p. 226, 2025.
L. S. K. G. Yaramolu, “Smart contracts in fintech: Revolutionizing financial transactions,” World Journal of Advanced Research and Reviews, vol. 26, no. 1, pp. 4149–4159, 2025.
M. A. S. Al-humaikani and L. B. A. Rahim, “A review on the verification approaches and tools used to verify the correctness of security algorithms and protocols,” International Journal of Advanced Computer Science and Application, vol. 10, no. 6, 2019.
N. Amit, S. Goldwasser, O. Paradise, and G. N. Rothblum, “Models that prove their own correctness,” arXiv, 2025.
R. Ait El Manssour, G. Kenison, M. Shirmohammadi, and A. Varonka, “Simple linear loops: Algebraic invariants and applications,” Proceedings of the ACM on Programming Languages, vol. 9, pp. 745– 771, 2025.
R. Cohen and E. Feron, “Verification and validation of convex optimization algorithms for model predictive control,” Journal of Guidance, Control, and Dynamics, vol. 7, pp. 78–83, 2020.
Shukla and V. Yadav, “Formal modelling and verification of effective probabilistic neural networks for load balancing in cloud environment,” Discover Computing, vol. 28, pp. 1–29, 2025.
T. Ferariu, P. Wadler, and O. Melkonian, “Validity, liquidity, and fidelity: Formal verification for smart contracts in Cardano,” OpenAccess Series in Informatics (OASIcs), vol. 6, pp. 1–21, 2025.
Z. Sbai, “Model checking deep neural networks: Opportunities and challenges,” Frontiers in Computer Science, vol. 7, 2025.
Z. Wang, Y. Lan, X. He, and J. Lv, “A formal verification approach for Linux kernel designing,” Technologies, vol. 12, no. 8, 2024.
Z. YOU, C. ZHANG, H. SUN, and Z. ZUO, “Program derivation and mechanized verification of edit distance algorithm,” Wuhan University Journal of Natural Sciences, vol. 30, no. 6, pp. 576–588, 2025.
