The B-Method is a formal specification and development methodology that ensures system correctness with a design-by-contract approach. However, translating these high-level specifications into C code introduces challenges, particularly in verifying that the generated code respects the specified properties. To address this, we propose a systematic translation process from the B-Method to ACSL, which enables the formal verification of the C code using Frama-C, a static analysis tool. The proposed method provides a set of ACSL specifications that correspond to B-Method abstractions, allowing for deductive verification of the C code to ensure compliance with safety and correctness requirements. A case study demonstrates the practical application of this translation strategy, showing its effectiveness in verifying a simple runner-counting system.