In recent years, code generation based on large language models is widely used in software development. However, due to the inherent stochasticity of the outputs from LLMs, proving the reliability of the code generated by LLMs has become a top priority. Formal verification is a powerful means that gives assurance of the correctness on the software. Before verification, the source code and requirements should be formalized into target specification language. Dafny is a programming language with built-in specification patterns. Dafny verification tools allow automated verification on Dafny specifications. This study aims to explore the ability of LLMs in translating Python into Dafny. To this end, this study introduces a prompt-based translation generation method employing both static translation and dynamic repair, along with a program-testing-based translation evaluating method. The static translation method considers three progressively refined prompting templates - Basic Prompting, Dafny Few-shot Prompting, Python2Dafny Few-shot Prompting – and performs single-step translation generation via LLMs; the dynamic repair method iteratively invokes LLMs for translation repair, incorporating error messages from the previous testing result into the prompt during each iteration. In evaluation, this study generates new testcase datasets by prompting LLMs on the occasion that there are no existing testcase datasets; with the datasets, this study uses Dafny test suite on translation results to perform evaluation. Our experiment employs state-of-the-art LLMs (notably GPT-4o and DeepSeek-V3) on HumanEval, MBPP and LeetCode datasets. Experimental results demonstrate that Python2Dafny Few-shot Prompting method and dynamic repair method effectively improves the correctness of Dafny translations generated by LLMs. Furthermore, this study contributes an analysis of translation quality determinants based on experimental evidence, and a discussion on both evaluation methodology and criteria.