text:
Các phương pháp hình thức
Trong ngành khoa học máy tính, các phương pháp hình thức là các kỹ thuật toán học cho việc đặc tả, phát triển và kiểm định các hệ thống phần mềm và phần cứng. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
Mục lục
Phân loại[sửa | sửa mã nguồn]
Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm định hình thức để tạo một chương trình theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính chất hoặc quá trình tinh chỉnh (refinement) từ đặc tả hình thức tới một chương trình. Đây có thể là lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí về an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các chứng minh hình thức hoàn toàn và được kiểm chứng bằng máy móc. Việc này có thể đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tồn cho các lỗi sai là cực kỳ cao (ví dụ, trong các phần quan trọng của thiết kế bộ vi xử lý).
Cùng với ngành con Ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức có thể được phân loại tương đối như sau:
- Ngữ nghĩa ký hiệu (Denotational semantics), trong đó ý nghĩa của một hệ thống được biểu diễn bằng lý thuyết toán học về miền xác định. Lợi điểm của những phương pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại ý nghĩa cho hệ thống; các phê phán chỉ ra rằng không phải hệ thống nào cũng có thể được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số.
- Ngữ nghĩ hoạt động (Operational semantics), trong đó, ý nghĩa của một hệ thống được biểu diễn bằng một chuỗi các hành động của một mô hình tính toán (giả thiết là) đơn giản hơn. Lợi điểm của phương pháp này là tính đơn giản của các mô hình tạo nên sự trong sáng của biểu diễn; nhược điểm là phương pháp này đã trì hoãn các vấn đề của ngữ nghĩa (ai định nghĩa ngữ nghĩa của các mô hình đơn giản hơn?)
- Ngữ nghĩa tiên đề (Axiomatic semantics), trong đó ý nghĩa của hệ thống được biểu diễn theo các tiền điều kiện (precondition) và hậu điều kiện (postcondition), đây lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ thống thực hiện một nhiệm vụ. Những người ủng hộ phương pháp này nói đến mối quan hệ của nó với lôgic kinh điển; những người phê phán nói rằng những ngữ nghĩa thuộc dạng này không thực sự mô tả xem hệ thống làm cái gì (chỉ là cái gì đúng trước đó và sau đó).
Sử dụng[sửa | sửa mã nguồn]
Các phương pháp hình thức có thể được áp dụng tại nhiều điểm khác nhau trong cả quá trình phát triển phần mềm. (Tuy có thể nói đến một quá trình phát triển bất kỳ, để thuận tiện, ta sẽ dùng các thuật ngữ của mô hình thác nước).
Đặc tả[sửa | sửa mã nguồn]
Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử dụng để hướng dẫn các hoạt động phát triển tiếp theo (xem các mục dưới); ngoài ra, nó có thể được sử dụng để kiểm định xem các yêu cầu cho hệ thống đang được phát triển đã được đặc tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong Báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô tả cú pháp ngôn ngữ lập trình (sau này được đặc tên là Backus normal form hay Backus-Naur form (BNF) (Dạng chuẩn tắc Backus));
Phát triển[sửa | sửa mã nguồn]
Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
- Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp cho việc dịch thẳng mã chạy được.
- Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện của đặc tả có thể trở thành các assertion
- If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become khẳng định (assertion') trong mã chạy được.
Kiểm định[sửa | sửa mã nguồn]
Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ sở cho việc chứng minh các tính chất của đặc tả.
Chứng minh của con người[sửa | sửa mã nguồn]
Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một chứng minh "tốt" là một chứng minh mà những người khác có thể đọc được và hiểu được.
Các phê phán đối với cách tiếp cận này nói rằng tính đa nghĩa cố hữu trong ngôn ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện; nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các chứng minh tốt đòi hỏi trình độ toán học cao.
Chứng minh tự động[sửa | sửa mã nguồn]
Ngược lại, ngày càng có nhiều quan tâm đến các chứng minh về tính đúng đắn của hệ thống bằng các phương tiện tự động. Các kỹ thuật tự động được phân thành hai loại chính:
- Chứng minh định lý tự động, trong đó, khi cho trước một mô tả về hệ thống, một tập các tiên đề lôgic và một tập các quy tắc suy luận, một hệ thống sẽ cố gắng tự xây dựng một chứng minh hình thức từ đầu.
- Kiểm tra mô hình, trong đó, một hệ thống kiểm định các tính chất nhất định bằng cách duyệt trong toàn bộ tất cả các trạng thái mà trong thời gian chạy, hệ thống có thể vào trạng thái đó.
Cả hai kỹ thuật trên đều hoạt động mà không cần đến sự hỗ trợ của con người. Các bộ chứng minh định lý tự động thường yêu cầu định hướng xem các tính chất nào là đáng quan tâm; các bộ kiểm tra mô hình có thể nhanh chóng sa lầy vào việc kiểm tra hàng triệu trạng thái không đáng quan tâm nếu không được cho trước một mô hình đủ trừu tượng.
Những người ủng hộ các hệ thống này cho rằng các kết quả của chúng có độ xác tính toán học cao hơn các chứng minh của con người, do tất cả các chi tiết buồn tẻ đã được kiểm định một cách có thuật toán. Việc huấn luyện cần thiết để có thể sử dụng được các hệ thống này cũng ít hơn đòi hỏi cần thiết cho việc tạo ra các chứng minh toán học tốt bằng tay. Nhờ đó, các kỹ thuật này có thể dùng được cho nhiều người hơn.
Những người phê phán cho rằng các hệ thống kiểu này giống như máy sấm truyền: chúng đưa ra các tuyên bố về sự thật nhưng lại không đưa ra giải thích nào về sự thực đó. Còn có cả vấn đề "kiểm định hệ kiểm định"; nếu chính chương trình tham gia công tác kiểm định không được chứng minh là đúng, thì có thể có lý do để nghi ngờ tính đúng đắn của các kết quả được tạo ra.
Phê phán[sửa | sửa mã nguồn]
Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho toàn bộ ngành các phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn, bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có các lỗi không được phát hiện. Ví dụ, trong kỹ thuật hàng không, các lỗi không được phát hiện có thể gây chết chóc, do đó các phương pháp hình thức được dùng rộng rãi trong ngành này hơn trong các lĩnh vực ứng dụng khác.
Các phương pháp hình thức và hệ thống ký hiệu[sửa | sửa mã nguồn]
- Abstract State Machines (ASMs)
- Alloy
- B-Method
- Process calculi
- Actor model
- Esterel
- Lustre
- Petri nets
- RAISE
- VDM
- Z notation
Xem thêm[sửa | sửa mã nguồn]
- Chứng minh định lý tự động
- Kiểm tra mô hình (Model checking)
- Kỹ nghệ phần mềm
- Các thảm họa kỹ nghệ phần mềm
Tham khảo[sửa | sửa mã nguồn]
- _ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, tháng 10 năm 1998
- _ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
- _ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, tháng 1 năm 2003
- _ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (tháng 4 năm 2002), pp. 256–290
- _ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, tháng 4 năm 1996
Liên kết ngoài[sửa | sửa mã nguồn]
Tiếng Anh:

markdown:
# Các phương pháp hình thức
Trong ngành
[khoa học máy tính](/wiki/Khoa_h%E1%BB%8Dc_m%C3%A1y_t%C3%ADnh), **các phương pháp hình thức** là các kỹ thuật toán học cho việc [đặc tả](/w/index.php?title=%C4%90%E1%BA%B7c_t%E1%BA%A3_h%C3%ACnh_th%E1%BB%A9c&action=edit&redlink=1), phát triển và [kiểm định](/w/index.php?title=Ki%E1%BB%83m_%C4%91%E1%BB%8Bnh_h%C3%ACnh_th%E1%BB%A9c&action=edit&redlink=1) các hệ thống [phần mềm](/wiki/Ph%E1%BA%A7n_m%E1%BB%81m) và [phần cứng](/wiki/Ph%E1%BA%A7n_c%E1%BB%A9ng). Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển [lò phản ứng hạt nhân](/wiki/L%C3%B2_ph%E1%BA%A3n_%E1%BB%A9ng_h%E1%BA%A1t_nh%C3%A2n) hay điều khiển [tên lửa](/wiki/T%C3%AAn_l%E1%BB%ADa), khi [an toàn](/w/index.php?title=An_to%C3%A0n&action=edit&redlink=1) hay [an ninh](/w/index.php?title=An_ninh&action=edit&redlink=1) có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức [yêu cầu](/wiki/Y%C3%AAu_c%E1%BA%A7u_(k%E1%BB%B9_thu%E1%BA%ADt)) và [đặc tả](/w/index.php?title=%C4%90%E1%BA%B7c_t%E1%BA%A3&action=edit&redlink=1) hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
## Mục lục
## Phân loại[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=1) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=1)]
Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
**Mức 0:** [Đặc tả hình thức](/w/index.php?title=%C4%90%E1%BA%B7c_t%E1%BA%A3_h%C3%ACnh_th%E1%BB%A9c&action=edit&redlink=1) có thể được thực hiện và rồi một chương trình được phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này có thể là lựa chọn hiệu quả nhất về mặt chi phí. **Mức 1:** Sử dụng [phát triển](/wiki/Ph%C3%A1t_tri%E1%BB%83n_ph%E1%BA%A7n_m%E1%BB%81m) và [kiểm định](/w/index.php?title=Ki%E1%BB%83m_%C4%91%E1%BB%8Bnh&action=edit&redlink=1) hình thức để tạo một chương trình theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính chất hoặc quá trình [tinh chỉnh](/w/index.php?title=Tinh_ch%E1%BB%89nh&action=edit&redlink=1) ( *refinement*) từ [đặc tả hình thức](/w/index.php?title=%C4%90%E1%BA%B7c_t%E1%BA%A3_h%C3%ACnh_th%E1%BB%A9c&action=edit&redlink=1) tới một chương trình. Đây có thể là lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí về [an toàn](/w/index.php?title=An_to%C3%A0n&action=edit&redlink=1) và [an ninh](/w/index.php?title=An_ninh&action=edit&redlink=1). **Mức 2:** Sử dụng các [bộ chứng minh định lý](/w/index.php?title=B%E1%BB%99_ch%E1%BB%A9ng_minh_%C4%91%E1%BB%8Bnh_l%C3%BD&action=edit&redlink=1) ( *theorem prover*) để thực hiện các chứng minh hình thức hoàn toàn và được kiểm chứng bằng máy móc. Việc này có thể đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tồn cho các lỗi sai là cực kỳ cao (ví dụ, trong các phần quan trọng của thiết kế bộ vi xử lý).
Cùng với ngành con
[Ngữ nghĩa hình thức của ngôn ngữ lập trình](/w/index.php?title=Ng%E1%BB%AF_ngh%C4%A9a_h%C3%ACnh_th%E1%BB%A9c_c%E1%BB%A7a_ng%C3%B4n_ng%E1%BB%AF_l%E1%BA%ADp_tr%C3%ACnh&action=edit&redlink=1), các phương pháp hình thức có thể được phân loại tương đối như sau: [Ngữ nghĩa ký hiệu](/w/index.php?title=Ng%E1%BB%AF_ngh%C4%A9a_k%C3%BD_hi%E1%BB%87u&action=edit&redlink=1)( *Denotational semantics*), trong đó ý nghĩa của một hệ thống được biểu diễn bằng lý thuyết toán học về [miền xác định](/w/index.php?title=L%C3%BD_thuy%E1%BA%BFt_mi%E1%BB%81n_x%C3%A1c_%C4%91%E1%BB%8Bnh&action=edit&redlink=1). Lợi điểm của những phương pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại ý nghĩa cho hệ thống; các phê phán chỉ ra rằng không phải hệ thống nào cũng có thể được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số. [Ngữ nghĩ hoạt động](/w/index.php?title=Ng%E1%BB%AF_ngh%C4%A9_ho%E1%BA%A1t_%C4%91%E1%BB%99ng&action=edit&redlink=1)( *Operational semantics*), trong đó, ý nghĩa của một hệ thống được biểu diễn bằng một chuỗi các hành động của một mô hình tính toán (giả thiết là) đơn giản hơn. Lợi điểm của phương pháp này là tính đơn giản của các mô hình tạo nên sự trong sáng của biểu diễn; nhược điểm là phương pháp này đã trì hoãn các vấn đề của ngữ nghĩa (ai định nghĩa ngữ nghĩa của các mô hình đơn giản hơn?) [Ngữ nghĩa tiên đề](/w/index.php?title=Ng%E1%BB%AF_ngh%C4%A9a_ti%C3%AAn_%C4%91%E1%BB%81&action=edit&redlink=1)( *Axiomatic semantics*), trong đó ý nghĩa của hệ thống được biểu diễn theo các [tiền điều kiện](/w/index.php?title=Ti%E1%BB%81n_%C4%91i%E1%BB%81u_ki%E1%BB%87n&action=edit&redlink=1)( *precondition*) và [hậu điều kiện](/w/index.php?title=H%E1%BA%ADu_%C4%91i%E1%BB%81u_ki%E1%BB%87n&action=edit&redlink=1)( *postcondition*), đây lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ thống thực hiện một nhiệm vụ. Những người ủng hộ phương pháp này nói đến mối quan hệ của nó với [lôgic](/wiki/Logic)kinh điển; những người phê phán nói rằng những ngữ nghĩa thuộc dạng này không thực sự mô tả xem hệ thống *làm*cái gì (chỉ là cái gì đúng trước đó và sau đó).
## Sử dụng[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=2) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=2)]
Các phương pháp hình thức có thể được áp dụng tại nhiều điểm khác nhau trong cả
[quá trình phát triển phần mềm](/wiki/Quy_tr%C3%ACnh_ph%C3%A1t_tri%E1%BB%83n_ph%E1%BA%A7n_m%E1%BB%81m). (Tuy có thể nói đến một quá trình phát triển bất kỳ, để thuận tiện, ta sẽ dùng các thuật ngữ của [mô hình thác nước](/wiki/M%C3%B4_h%C3%ACnh_th%C3%A1c_n%C6%B0%E1%BB%9Bc)).
### Đặc tả[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=3) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=3)]
Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử dụng để hướng dẫn các hoạt động phát triển tiếp theo (xem các mục dưới); ngoài ra, nó có thể được sử dụng để kiểm định xem các yêu cầu cho hệ thống đang được phát triển đã được đặc tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong Báo cáo
[ALGOL 60](/w/index.php?title=ALGOL_60&action=edit&redlink=1), [John Backus](/w/index.php?title=John_Backus&action=edit&redlink=1) đã trình bày một hệ thống ký hiệu hình thức để mô tả cú pháp ngôn ngữ lập trình (sau này được đặc tên là [Backus normal form](/w/index.php?title=Backus_normal_form&action=edit&redlink=1) hay [Backus-Naur form](/w/index.php?title=Backus-Naur_form&action=edit&redlink=1) (BNF) ( *Dạng chuẩn tắc Backus*));
### Phát triển[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=4) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=4)]
Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
- Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp cho việc dịch thẳng mã chạy được.
- Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện của đặc tả có thể trở thành các
[assertion](/w/index.php?title=Assertion&action=edit&redlink=1)
- If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become
[khẳng định](/w/index.php?title=Kh%E1%BA%B3ng_%C4%91%E1%BB%8Bnh_(t%C3%ADnh_to%C3%A1n)&action=edit&redlink=1)( *assertion') trong mã chạy được.*
### Kiểm định[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=5) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=5)]
Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ sở cho việc
[chứng minh](/w/index.php?title=Ch%E1%BB%A9ng_minh&action=edit&redlink=1) các tính chất của đặc tả.
#### Chứng minh của con người[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=6) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=6)]
Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức
[chứng minh toán học](/wiki/Ch%E1%BB%A9ng_minh_to%C3%A1n_h%E1%BB%8Dc): viết tay hoặc đánh máy nội dung bằng [ngôn ngữ tự nhiên](/wiki/Ng%C3%B4n_ng%E1%BB%AF_t%E1%BB%B1_nhi%C3%AAn), với mức độ phi hình thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một chứng minh "tốt" là một chứng minh mà những người khác có thể đọc được và hiểu được.
Các phê phán đối với cách tiếp cận này nói rằng
[tính đa nghĩa](/w/index.php?title=T%C3%ADnh_%C4%91a_ngh%C4%A9a&action=edit&redlink=1) cố hữu trong ngôn ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện; nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các chứng minh tốt đòi hỏi trình độ toán học cao.
#### Chứng minh tự động[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=7) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=7)]
Ngược lại, ngày càng có nhiều quan tâm đến các chứng minh về tính đúng đắn của hệ thống bằng các phương tiện tự động. Các kỹ thuật tự động được phân thành hai loại chính:
[Chứng minh định lý tự động](/w/index.php?title=Ch%E1%BB%A9ng_minh_%C4%91%E1%BB%8Bnh_l%C3%BD_t%E1%BB%B1_%C4%91%E1%BB%99ng&action=edit&redlink=1), trong đó, khi cho trước một mô tả về hệ thống, một tập các tiên đề lôgic và một tập các quy tắc suy luận, một hệ thống sẽ cố gắng tự xây dựng một chứng minh hình thức từ đầu. [Kiểm tra mô hình](/w/index.php?title=Ki%E1%BB%83m_tra_m%C3%B4_h%C3%ACnh&action=edit&redlink=1), trong đó, một hệ thống kiểm định các tính chất nhất định bằng cách duyệt trong toàn bộ tất cả các trạng thái mà trong thời gian chạy, hệ thống có thể vào trạng thái đó.
Cả hai kỹ thuật trên đều hoạt động mà không cần đến sự hỗ trợ của con người. Các bộ chứng minh định lý tự động thường yêu cầu định hướng xem các tính chất nào là đáng quan tâm; các bộ kiểm tra mô hình có thể nhanh chóng sa lầy vào việc kiểm tra hàng triệu trạng thái không đáng quan tâm nếu không được cho trước một mô hình đủ trừu tượng.
Những người ủng hộ các hệ thống này cho rằng các kết quả của chúng có độ xác tính toán học cao hơn các chứng minh của con người, do tất cả các chi tiết buồn tẻ đã được kiểm định một cách có thuật toán. Việc huấn luyện cần thiết để có thể sử dụng được các hệ thống này cũng ít hơn đòi hỏi cần thiết cho việc tạo ra các chứng minh toán học tốt bằng tay. Nhờ đó, các kỹ thuật này có thể dùng được cho nhiều người hơn.
Những người phê phán cho rằng các hệ thống kiểu này giống như
[máy sấm truyền](/w/index.php?title=M%C3%A1y_s%E1%BA%A5m_truy%E1%BB%81n&action=edit&redlink=1): chúng đưa ra các tuyên bố về sự thật nhưng lại không đưa ra giải thích nào về sự thực đó. Còn có cả vấn đề "kiểm định hệ kiểm định"; nếu chính chương trình tham gia công tác kiểm định không được chứng minh là đúng, thì có thể có lý do để nghi ngờ tính đúng đắn của các kết quả được tạo ra.
## Phê phán[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=8) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=8)]
Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho toàn bộ ngành các phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn, bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có các lỗi không được phát hiện. Ví dụ, trong
[kỹ thuật hàng không](/w/index.php?title=K%E1%BB%B9_thu%E1%BA%ADt_h%C3%A0ng_kh%C3%B4ng&action=edit&redlink=1), các lỗi không được phát hiện có thể gây chết chóc, do đó các phương pháp hình thức được dùng rộng rãi trong ngành này hơn trong các lĩnh vực ứng dụng khác.
## Các phương pháp hình thức và hệ thống ký hiệu[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=9) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=9)] [Abstract State Machines](/w/index.php?title=Abstract_State_Machines&action=edit&redlink=1)(ASMs) [Alloy](/w/index.php?title=Alloy_language&action=edit&redlink=1) [B-Method](/w/index.php?title=B-Method&action=edit&redlink=1) [Process calculi](/w/index.php?title=Process_calculi&action=edit&redlink=1) [Actor model](/w/index.php?title=Actor_model&action=edit&redlink=1) [Esterel](/w/index.php?title=Esterel&action=edit&redlink=1) [Lustre](/w/index.php?title=Lustre_programming_language&action=edit&redlink=1) [Petri nets](/w/index.php?title=Petri_nets&action=edit&redlink=1) [RAISE](/w/index.php?title=Ng%C3%B4n_ng%E1%BB%AF_%C4%91%E1%BA%B7c_t%E1%BA%A3_RAISE&action=edit&redlink=1) [VDM](/w/index.php?title=Vienna_Development_Method&action=edit&redlink=1) [Z notation](/w/index.php?title=Z_notation&action=edit&redlink=1)
## Xem thêm[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=10) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=10)] [Chứng minh định lý tự động](/w/index.php?title=Ch%E1%BB%A9ng_minh_%C4%91%E1%BB%8Bnh_l%C3%BD_t%E1%BB%B1_%C4%91%E1%BB%99ng&action=edit&redlink=1) [Kiểm tra mô hình](/w/index.php?title=Ki%E1%BB%83m_tra_m%C3%B4_h%C3%ACnh&action=edit&redlink=1)( *Model checking*) [Kỹ nghệ phần mềm](/wiki/C%C3%B4ng_ngh%E1%BB%87_ph%E1%BA%A7n_m%E1%BB%81m) [Các thảm họa kỹ nghệ phần mềm](/w/index.php?title=Th%E1%BB%83_lo%E1%BA%A1i:Th%E1%BA%A3m_h%E1%BB%8Da_k%E1%BB%B9_ngh%E1%BB%87_ph%E1%BA%A7n_m%E1%BB%81m&action=edit&redlink=1)
## Tham khảo[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=11) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=11)] [Sten Agerholm and Peter G. Larsen,](#ref_AgerholmLarsen1998) _ ["A Lightweight Approach to Formal Methods"](http://home0.inet.tele.dk/pgl/fmtrends98.pdf), In *Proceedings of the International Workshop on Current Trends in Applied Formal Methods*, Boppard, Germany, Springer-Verlag, tháng 10 năm 1998 [Richard Denney,](#ref_Denney2005) _ *Succeeding with Use Cases: Working Smart to Deliver Quality*, Addison-Wesley Professional Publishing, 2005, [ISBN 0-321-31643-6](/wiki/%C4%90%E1%BA%B7c_bi%E1%BB%87t:Ngu%E1%BB%93n_s%C3%A1ch/0321316436). [Vinu George and Rayford Vaughn,](#ref_GeorgeVaughn2003) _ ["Application of Lightweight Formal Methods in Requirement Engineering"](http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html), *Crosstalk: The Journal of Defense Software Engineering*, tháng 1 năm 2003 [Daniel Jackson,](#ref_Jackson2002) _ ["Alloy: A Lightweight Object Modelling Notation"](http://people.csail.mit.edu/dnj/publications/alloy-journal.pdf), *ACM Transactions on Software Engineering and Methodology (TOSEM)*, Volume 11, Issue 2 (tháng 4 năm 2002), pp. 256–290 [Daniel Jackson and Jeannette Wing,](#ref_JacksonWing1996) _ ["Lightweight Formal Methods"](http://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html), *IEEE Computer*, tháng 4 năm 1996
## Liên kết ngoài[
[sửa](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&veaction=edit&vesection=12) | [sửa mã nguồn](/w/index.php?title=C%C3%A1c_ph%C6%B0%C6%A1ng_ph%C3%A1p_h%C3%ACnh_th%E1%BB%A9c&action=edit§ion=12)]
Tiếng Anh:
[Formal methods publications](http://vl.fmnet.info/pubs/) [Virtual Library formal methods](http://vl.fmnet.info/) [Who's who in formal methods](http://vl.fmnet.info/whos-who/) [Meetings](http://vl.fmnet.info/meetings/) [Organizations](http://vl.fmnet.info/orgs/) [Companies](http://vl.fmnet.info/companies/)
|
|
· · · · · · · · · · · · · · · · Các phương pháp hình thức · · · · · · ·
Chú ý: khoa học máy tính còn có thể được chia thành nhiều chủ đề hay nhiều lĩnh vực khác dựa theo
|
|


text:
Greimerath
Bách khoa toàn thư mở Wikipedia
Đối với Greimerath ở huyện Trier-Saarburg, xem Greimerath, Trier-Saarburg.
Greimerath là một đô thị ở huyện Bernkastel-Wittlich, trong bang Rheinland-Pfalz, Đô thị Greimerath có diện tích 3,75 km², dân số thời điểm ngày 31 tháng 12 năm 2006 là 233 người.
Tham khảo[sửa | sửa mã nguồn]
- “Statistisches Landesamt Rheinland-Pfalz”. Truy cập ngày 2 tháng 9 năm 2007.

markdown:
# Greimerath
Bách khoa toàn thư mở Wikipedia
|
|Greimerath
|
|Huy hiệu |
|Vị trí
|
|Hành chính
|
|[Đức](/wiki/%C4%90%E1%BB%A9c) [Bang](/wiki/Bang_c%E1%BB%A7a_%C4%90%E1%BB%A9c) [Rheinland-Pfalz](/wiki/Rheinland-Pfalz) [Huyện](/wiki/Huy%E1%BB%87n_c%E1%BB%A7a_%C4%90%E1%BB%A9c) [Bernkastel-Wittlich](/wiki/Bernkastel-Wittlich) [Verbandsgemeinde](/w/index.php?title=Verbandsgemeinde&action=edit&redlink=1) [Thị trưởng](/wiki/Burgomaster) **Số liệu thống kê cơ bản** [Diện tích](/wiki/Di%E1%BB%87n_t%C3%ADch) [Cao độ](/wiki/Cao_%C4%91%E1%BB%99) [Dân số](/wiki/D%C3%A2n_s%E1%BB%91) *(31/12/2006)* [Mật độ](/wiki/M%E1%BA%ADt_%C4%91%E1%BB%99_d%C3%A2n_s%E1%BB%91) **Các thông tin khác** [Múi giờ](/wiki/M%C3%BAi_gi%E1%BB%9D) [CET](/wiki/Gi%E1%BB%9D_Trung_%C3%82u)/ [CEST](/wiki/Gi%E1%BB%9D_m%C3%B9a_H%C3%A8_Trung_%C3%82u)( [UTC+1](/wiki/UTC%2B1)/ [+2](/wiki/UTC%2B2)) [Biển số xe](/wiki/Bi%E1%BB%83n_s%E1%BB%91_xe) [Mã bưu chính](/wiki/Danh_s%C3%A1ch_m%C3%A3_b%C6%B0u_ch%C3%ADnh_%E1%BB%9F_%C4%90%E1%BB%A9c) [Mã vùng](/w/index.php?title=M%C3%A3_v%C3%B9ng_%E1%BB%9F_%C4%90%E1%BB%A9c&action=edit&redlink=1) [Website](/wiki/Website) [www.greimerath.de](http://www.greimerath.de/)
Đối với Greimerath ở huyện Trier-Saarburg, xem
[Greimerath, Trier-Saarburg](/wiki/Greimerath,_Trier-Saarburg). **Greimerath** là một [đô thị](/w/index.php?title=%C4%90%C3%B4_th%E1%BB%8B_c%E1%BB%A7a_%C4%90%E1%BB%A9c&action=edit&redlink=1) ở [huyện Bernkastel-Wittlich](/wiki/Bernkastel-Wittlich), trong [bang](/wiki/Bang_c%E1%BB%A7a_%C4%90%E1%BB%A9c) [Rheinland-Pfalz](/wiki/Rheinland-Pfalz), Đô thị Greimerath có [diện tích](/wiki/Di%E1%BB%87n_t%C3%ADch) 3,75 [km²](/wiki/Km%C2%B2), [dân số](/wiki/D%C3%A2n_s%E1%BB%91) thời điểm ngày [31 tháng 12](/wiki/31_th%C3%A1ng_12) năm [2006](/wiki/2006) là 233 người.
## Tham khảo[
[sửa](/w/index.php?title=Greimerath&veaction=edit&vesection=1) | [sửa mã nguồn](/w/index.php?title=Greimerath&action=edit§ion=1)] [“Statistisches Landesamt Rheinland-Pfalz”](http://www.infothek.statistik.rlp.de). Truy cập ngày 2 tháng 9 năm 2007.

WARC-Type: response

Content-Type: application/http; msgtype=response

Set-Cookie: GeoIP=US:VA:Ashburn:39.04:-77.49:v4; Path=/; secure; Domain=.wikipedia.org

Connection: close

X-Content-Type-Options: nosniff

Cache-Control: private, s-maxage=0, max-age=0, must-revalidate

X-Cache-Status: miss

P3P: CP="This is not a P3P policy! See https://vi.wikipedia.org/wiki/%C4%90%E1%BA%B7c_bi%E1%BB%87t:CentralAutoLogin/P3P for more info."

Via: 1.1 varnish, 1.1 varnish

Content-Language: vi

X-UA-Compatible: IE=Edge

X-Cache: cp1055 miss, cp1065 miss

Vary: Accept-Encoding,Cookie,Authorization

Content-Type: text/html; charset=UTF-8

Accept-Ranges: bytes


text:
Mila (tỉnh)
Bách khoa toàn thư mở Wikipedia
Mila (tiếng Ả Rập: ولاية ميلة ) là một wilaya của Algérie, tỉnh lỵ là Mila. Các đô thị khác có Telerghma, Grarem Gouga, Hamala và Rouached.
Các đơn vị hành chính[sửa | sửa mã nguồn]
Tỉnh này gồm 13 huyện và 32 đô thị. Các huyện bao gồm:
- Chelghoum Laïd
- Grarem Gouga
- Sidi Merouane
- Oued Endja
- Teleghma
- Ferdjioua
- Tadjenanet
- Terrai Bainem
- Rouached
- Tassadane Haddada
- Aïn Beida Harriche
- Bouhatem
- Mila
Tham khảo[sửa | sửa mã nguồn]
- ^ Office National des Statistiques, Recensement General de la Population et de l’Habitat 2008 Kết quả điều tra dân số sơ bộ năm 2008. Truy cập ngày 2 tháng 7 năm 2008.

markdown:
# Mila (tỉnh)
Bách khoa toàn thư mở Wikipedia
|
|Tỉnh Mila
|
|ولاية ميلة
|
|![]()
*Bản đồ Algérie với tỉnh Mila* [Mã tỉnh](/w/index.php?title=T%E1%BB%89nh_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1) [Mã vùng](/w/index.php?title=M%C3%A3_v%C3%B9ng&action=edit&redlink=1) **Hành chính** [Thủ phủ](/wiki/Th%E1%BB%A7_ph%E1%BB%A7) [Mila, Algérie](/w/index.php?title=Mila,_Alg%C3%A9rie&action=edit&redlink=1) [Các huyện](/w/index.php?title=Huy%E1%BB%87n_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1) [Các đô thị](/w/index.php?title=%C4%90%C3%B4_th%E1%BB%8B_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1) **Số liệu thống kê cơ bản** **Diện tích** [9.375](/w/index.php?title=1_E%2B9_m%C2%B2&action=edit&redlink=1) [km²](/wiki/Kil%C3%B4m%C3%A9t_vu%C3%B4ng)(3.619,7 [dặm vuông](/w/index.php?title=D%E1%BA%B7m_Anh_vu%C3%B4ng&action=edit&redlink=1)) **Dân số** [[1]](#cite_note-Alg2008RGPH-1) *(* [2008](/wiki/2008)) [Mật độ](/wiki/M%E1%BA%ADt_%C4%91%E1%BB%99_d%C3%A2n_s%E1%BB%91) **Mila** ( [tiếng Ả Rập](/wiki/Ti%E1%BA%BFng_%E1%BA%A2_R%E1%BA%ADp): **ولاية ميلة** ) là một [wilaya](/w/index.php?title=T%E1%BB%89nh_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1) của [Algérie](/wiki/Alg%C3%A9rie), tỉnh lỵ là [Mila](/w/index.php?title=Mila,_Alg%C3%A9rie&action=edit&redlink=1). Các đô thị khác có [Telerghma](/w/index.php?title=Telerghma&action=edit&redlink=1), [Grarem Gouga](/w/index.php?title=Grarem&action=edit&redlink=1), [Hamala](/w/index.php?title=Hamala,_Alg%C3%A9rie&action=edit&redlink=1) và [Rouached](/wiki/Rouached).
## Các đơn vị hành chính[
[sửa](/w/index.php?title=Mila_(t%E1%BB%89nh)&veaction=edit&vesection=1) | [sửa mã nguồn](/w/index.php?title=Mila_(t%E1%BB%89nh)&action=edit§ion=1)]
Tỉnh này gồm 13
[huyện](/w/index.php?title=Huy%E1%BB%87n_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1) và 32 [đô thị](/w/index.php?title=%C4%90%C3%B4_th%E1%BB%8B_c%E1%BB%A7a_Alg%C3%A9rie&action=edit&redlink=1). Các huyện bao gồm: [Chelghoum Laïd](/w/index.php?title=Chelghoum_La%C3%AFd_(huy%E1%BB%87n)&action=edit&redlink=1) [Grarem Gouga](/w/index.php?title=Grarem_Gouga_(huy%E1%BB%87n)&action=edit&redlink=1) [Sidi Merouane](/w/index.php?title=Sidi_Merouane_(huy%E1%BB%87n)&action=edit&redlink=1) [Oued Endja](/w/index.php?title=Oued_Endja_(huy%E1%BB%87n)&action=edit&redlink=1) [Teleghma](/w/index.php?title=Teleghma_(huy%E1%BB%87n)&action=edit&redlink=1) [Ferdjioua](/w/index.php?title=Ferdjioua_(huy%E1%BB%87n)&action=edit&redlink=1) [Tadjenanet](/w/index.php?title=Tadjenanet_(huy%E1%BB%87n)&action=edit&redlink=1) [Terrai Bainem](/w/index.php?title=Terrai_Bainem_(huy%E1%BB%87n)&action=edit&redlink=1) [Rouached](/w/index.php?title=Rouached_(huy%E1%BB%87n)&action=edit&redlink=1) [Tassadane Haddada](/w/index.php?title=Tassadane_Haddada_(huy%E1%BB%87n)&action=edit&redlink=1) [Aïn Beida Harriche](/w/index.php?title=A%C3%AFn_Beida_Harriche_(huy%E1%BB%87n)&action=edit&redlink=1) [Bouhatem](/w/index.php?title=Bouhatem_(huy%E1%BB%87n)&action=edit&redlink=1) [Mila](/w/index.php?title=Mila_(huy%E1%BB%87n)&action=edit&redlink=1)
## Tham khảo[
[sửa](/w/index.php?title=Mila_(t%E1%BB%89nh)&veaction=edit&vesection=2) | [sửa mã nguồn](/w/index.php?title=Mila_(t%E1%BB%89nh)&action=edit§ion=2)] [^](#cite_ref-Alg2008RGPH_1-0) [Office National des Statistiques, Recensement General de la Population et de l’Habitat 2008](http://rgph2008.ons.dz/resultat/histo.htm)Kết quả điều tra dân số sơ bộ năm 2008. Truy cập ngày 2 tháng 7 năm 2008.
|
|

X-Cache: cp1067 miss, cp1065 miss


text:
Pappophorum
Bách khoa toàn thư mở Wikipedia
Pappophorum là một chi thực vật có hoa trong họ Hòa thảo (Poaceae).[1]
Loài[sửa | sửa mã nguồn]
Chi Pappophorum gồm các loài:
Chú thích[sửa | sửa mã nguồn]
- ^ The Plant List (2010). “Pappophorum”. Truy cập ngày 26 tháng 9 năm 2013.
Liên kết ngoài[sửa | sửa mã nguồn]
- Phương tiện liên quan tới Pappophorum tại Wikimedia Commons
- Dữ liệu liên quan tới Pappophorum tại Wikispecies

markdown:
*Pappophorum*
Bách khoa toàn thư mở Wikipedia
|
|Pappophorum
|
|[Giới](/wiki/Gi%E1%BB%9Bi_(sinh_h%E1%BB%8Dc))( *regnum*) [Plantae](/wiki/Th%E1%BB%B1c_v%E1%BA%ADt) [Angiospermae](/wiki/Th%E1%BB%B1c_v%E1%BA%ADt_c%C3%B3_hoa) [Monocots](/wiki/Th%E1%BB%B1c_v%E1%BA%ADt_m%E1%BB%99t_l%C3%A1_m%E1%BA%A7m) [Commelinids](/wiki/Nh%C3%A1nh_Th%C3%A0i_l%C3%A0i) [Bộ](/wiki/B%E1%BB%99_(sinh_h%E1%BB%8Dc))( *ordo*) [Poales](/wiki/B%E1%BB%99_H%C3%B2a_th%E1%BA%A3o) [Họ](/wiki/H%E1%BB%8D_(sinh_h%E1%BB%8Dc))( *familia*) [Poaceae](/wiki/H%E1%BB%8D_H%C3%B2a_th%E1%BA%A3o) [Chi](/wiki/Chi_(sinh_h%E1%BB%8Dc))( *genus*) **Pappophorum** * là một chi Pappophorum* [thực vật có hoa](/wiki/Th%E1%BB%B1c_v%E1%BA%ADt_c%C3%B3_hoa)trong [họ Hòa thảo](/wiki/H%E1%BB%8D_H%C3%B2a_th%E1%BA%A3o)(Poaceae). [[1]](#cite_note-1)
## Loài[
[sửa](/w/index.php?title=Pappophorum&veaction=edit&vesection=1) | [sửa mã nguồn](/w/index.php?title=Pappophorum&action=edit§ion=1)]
Chi
*Pappophorum* gồm các loài:
## Chú thích[
[sửa](/w/index.php?title=Pappophorum&veaction=edit&vesection=2) | [sửa mã nguồn](/w/index.php?title=Pappophorum&action=edit§ion=2)] **The Plant List (2010).** [^](#cite_ref-1) [“](http://www.theplantlist.org/browse/A/Compositae/Pappophorum). Truy cập ngày 26 tháng 9 năm 2013. *Pappophorum*”
## Liên kết ngoài[
[sửa](/w/index.php?title=Pappophorum&veaction=edit&vesection=3) | [sửa mã nguồn](/w/index.php?title=Pappophorum&action=edit§ion=3)]
Phương tiện liên quan tới
[Pappophorum](https://commons.wikimedia.org/wiki/Category:Pappophorum)tại [Wikimedia Commons](/wiki/Wikimedia_Commons)
Dữ liệu liên quan tới
[Pappophorum](https://species.wikimedia.org/wiki/Pappophorum)tại [Wikispecies](/wiki/Wikispecies)


text:
Scorpion II
Scorpion, cũng được gọi là Vua Scorpion (Vua Bò Cạp) hay Scorpion II, là một trong hai vị vua mang tên Scorpion ở vùng Thượng Ai Cập, vào thời Tiền triều đại Ai Cập.
Tên và chức danh[sửa | sửa mã nguồn]
Tên và chức danh của vị vua này không được biết đầy đủ. Theo nhận định của nhiều học giả (T. Wilkinson, Renée Friedman, Bruce Trigger), thời Scorpion II là thời kỳ Ai Cập bị chia thành nhiều vương quốc nhỏ và họ đánh nhau liên tục trong nhiều năm.
Bằng chứng duy nhất chứng minh sự có mặt của vua Scorpion II là Scorpion Macehead, được James E. Quibell và Frederick W. Green tìm thấy trong một ngôi đền tại Nekhen (Hierakonpolis) vào các năm 1897–1898[1]. Đây có lẽ là bức phù điêu, mô tả vị vua này đang cày ruộng (ông ta có chiếc cuốc đang cày ruộng, phía sau là người hầu đang gieo hạt)[2]. Các phiến đá được khai quật tại Tarkhan và Minshat Abu Omar, miêu tả vua (dưới dạng con bò cạp) đang chiến đấu với kẻ thù. Một cuộc khai quật nữa ở ghềnh thứ hai của sông Nile, cách không xa Nasser-reservoire tại Gebel Sheikh Suliman (Sudan), tìm thấy một phiến đá mô tả con bò cạp đang bước qua xác kẻ thù bị giết chết. Cái chết của họ (kẻ thù) được mô tả là bị trúng tên, cơ thể bị dốc ngược (hướng chân lên trời); hai người nữa còn cầm cung bắn tên. Vì nhận diện những người chết này đang cầm cung và có lông đà điểu mà người ta xác định đó là người Nubia. Các con bò cạp sau chiến thắng đã tiến hành "hiến tế" kẻ thù người Nubia, bằng chứng là còn lại một con dao, một sợi dây - có lẽ để siết cổ kẻ thù (hay trói lại) rồi giết chết. Toàn bộ khung cảnh được hiểu như là vua Scorpion II ăn mừng chiến thắng của mình chống lại các người Nubians thù địch[3]. Biểu tượng "con bò cạp" trên cái cày (có chỗ ghi là chùy) đại diện cho quyền lực của vua.
Trị vì[sửa | sửa mã nguồn]
Dưới thời vua Scorpion II, các bảng Hunters Palette, các Palette Libya và Narmer Palette, cho thấy một nền nông nghiệp sơ khai được hình thành. Trong bảng, người ta thấy sông, cây cỏ và muôn thú; hệ thống kênh tưới nước ở Ai Cập cổ. Người Ai cập thời kỳ này thờ đa thần, nhưng họ lại thờ các vị thần quan trọng như: Horus, Seth, Min, Nemty, Nekhbet, Bat and Wepwawet. Họ cũng có thờ con vật, nhiều nhất là con rắn cổ beo; hai con chó Palette...... Một điểm mới là đã "xuất hiện sinh vật có cánh" mà người Ai Cập cổ gọi là "Chimeras có cánh", có tên là Sefer - đại diện cho quyền lực và bao lực, mà nhiều học giả nghi rằng nó có nguồn gốc từ Lưỡng Hà. Một bằng chứng nữa chứng minh ảnh hưởng của Lưỡng Hà qua Ai Cập, là hình một chiến binh chiến đấu hai con sư tử với hai bàn tay trần của mìn. Ngay cả nhà vua cũng nuôi 2 con sư tử ở hai bên hông, 2 con nhỏ đặt ở lòng bàn tay. Ở tại Minshat Abu Omar, Hierakonpolis và Naqada; người ta nhận thấy kiến trúc ngôi mộ và các mặt hàng được giao dịch (chẳng hạn như các công cụ, vòng cổ hạt và con dấu xi lanh) chứng minh một ảnh hưởng mạnh mẽ và sâu rộng đáng ngạc nhiên của văn hóa Lưỡng Hà và tôn giáo của thời kỳ đầu người Ai Cập. Các ngôi mộ được xây dựng với kết cấu rất phức tạp và ổn định đã được sao chép rõ ràng từ các tòa nhà Lưỡng Hà. Thậm chí, một số học giả đang cho rằng các thủ lĩnh cai trị Ai Cập, có lẽ xuất thân từ vùng đất Lưỡng Hà[4].
Tham khảo[sửa | sửa mã nguồn]
- ^ "The Narmer Palette", The Ancient Egypt, retrieved ngày 19 tháng 9 năm 2007
- ^ Krzysztof Marek Ciałowicz: La Naissance d'un Royaume:. L'Egypte des la periode prédynastique à la fin de la Ière Dynastie Inst. Archeologii Uniw. Jagiellońskiego, Kraków 2001, ISBN 83-7188-483-4, p. 97 & 98.
- ^ Werner Kaiser, Günter Dreyer: Umm el-Qaab: Nachuntersuchungen im frühzeitlichen Königsfriedhof. 2. Vorbericht. Trong: MDAIK Nr. 38. von Zabern, Mainz 1982, ISBN 3-8053-0552-4, p.70.
- ^ Krzysztof Marek Ciałowicz: La Naissance d'un Royaume:. L'Egypte des la periode prédynastique à la fin de la Ière Dynastie Inst. Archeologii Uniw. Jagiellońskiego, Kraków 2001, ISBN 83-7188-483-4, p. 97 & 98.

markdown:
# Scorpion II
|Bài viết này
|không được .
|
|Scorpion II
|Tiên vương:
||
||Kế vị:
|
**Scorpion**, cũng được gọi là **Vua Scorpion** ( *Vua Bò Cạp*) hay **Scorpion II**, là một trong hai vị vua mang tên Scorpion ở vùng [Thượng Ai Cập](/wiki/Th%C6%B0%E1%BB%A3ng_Ai_C%E1%BA%ADp), vào thời [Tiền triều đại Ai Cập](/w/index.php?title=Ti%E1%BB%81n_tri%E1%BB%81u_%C4%91%E1%BA%A1i_Ai_C%E1%BA%ADp&action=edit&redlink=1).
## Tên và chức danh[
[sửa](/w/index.php?title=Scorpion_II&veaction=edit&vesection=1) | [sửa mã nguồn](/w/index.php?title=Scorpion_II&action=edit§ion=1)]
Tên và chức danh của vị vua này không được biết đầy đủ. Theo nhận định của nhiều học giả (T. Wilkinson, Renée Friedman, Bruce Trigger), thời Scorpion II là thời kỳ Ai Cập bị chia thành nhiều vương quốc nhỏ và họ đánh nhau liên tục trong nhiều năm.
Bằng chứng duy nhất chứng minh sự có mặt của vua Scorpion II là
*Scorpion Macehead*, được James E. Quibell và Frederick W. Green tìm thấy trong một ngôi đền tại Nekhen (Hierakonpolis) vào các năm 1897–1898 . Đây có lẽ là bức phù điêu, mô tả vị vua này đang cày ruộng (ông ta có chiếc cuốc đang cày ruộng, phía sau là người hầu đang gieo hạt) [1] . Các phiến đá được khai quật tại Tarkhan và Minshat Abu Omar, miêu tả vua (dưới dạng con bò cạp) đang chiến đấu với kẻ thù. Một cuộc khai quật nữa ở ghềnh thứ hai của sông Nile, cách không xa Nasser-reservoire tại Gebel Sheikh Suliman (Sudan), tìm thấy một phiến đá mô tả con bò cạp đang bước qua xác kẻ thù bị giết chết. Cái chết của họ (kẻ thù) được mô tả là bị trúng tên, cơ thể bị dốc ngược (hướng chân lên trời); hai người nữa còn cầm cung bắn tên. Vì nhận diện những người chết này đang cầm cung và có lông đà điểu mà người ta xác định đó là người Nubia. Các [[2]](#cite_note-2) *con bò cạp*sau chiến thắng đã tiến hành "hiến tế" kẻ thù người Nubia, bằng chứng là còn lại một con dao, một sợi dây - có lẽ để siết cổ kẻ thù (hay trói lại) rồi giết chết. Toàn bộ khung cảnh được hiểu như là vua Scorpion II ăn mừng chiến thắng của mình chống lại các người Nubians thù địch . Biểu tượng "con bò cạp" trên cái cày (có chỗ ghi là [[3]](#cite_note-3) *chùy*) đại diện cho quyền lực của vua.
## Trị vì[
[sửa](/w/index.php?title=Scorpion_II&veaction=edit&vesection=2) | [sửa mã nguồn](/w/index.php?title=Scorpion_II&action=edit§ion=2)]
Dưới thời vua Scorpion II, các bảng
*Hunters Palette,* các *Palette Libya* và *Narmer Palette*, cho thấy một nền nông nghiệp sơ khai được hình thành. Trong bảng, người ta thấy sông, cây cỏ và muôn thú; hệ thống kênh tưới nước ở Ai Cập cổ. Người Ai cập thời kỳ này thờ đa thần, nhưng họ lại thờ các vị thần quan trọng như: Horus, Seth, Min, Nemty, Nekhbet, Bat and Wepwawet. Họ cũng có thờ con vật, nhiều nhất là con rắn cổ beo; hai con chó Palette...... Một điểm mới là đã "xuất hiện sinh vật có cánh" mà người Ai Cập cổ gọi là "Chimeras có cánh", có tên là *Sefer* - đại diện cho quyền lực và bao lực, mà nhiều học giả nghi rằng nó có nguồn gốc từ Lưỡng Hà. Một bằng chứng nữa chứng minh ảnh hưởng của Lưỡng Hà qua Ai Cập, là hình một chiến binh chiến đấu hai con sư tử với hai bàn tay trần của mìn. Ngay cả nhà vua cũng nuôi 2 con sư tử ở hai bên hông, 2 con nhỏ đặt ở lòng bàn tay. Ở tại Minshat Abu Omar, Hierakonpolis và Naqada; người ta nhận thấy kiến trúc ngôi mộ và các mặt hàng được giao dịch (chẳng hạn như các công cụ, vòng cổ hạt và con dấu xi lanh) chứng minh một ảnh hưởng mạnh mẽ và sâu rộng đáng ngạc nhiên của văn hóa Lưỡng Hà và tôn giáo của thời kỳ đầu người Ai Cập. Các ngôi mộ được xây dựng với kết cấu rất phức tạp và ổn định đã được sao chép rõ ràng từ các tòa nhà Lưỡng Hà. Thậm chí, một số học giả đang cho rằng các thủ lĩnh cai trị Ai Cập, có lẽ xuất thân từ vùng đất Lưỡng Hà . [4]
## Tham khảo[
[sửa](/w/index.php?title=Scorpion_II&veaction=edit&vesection=3) | [sửa mã nguồn](/w/index.php?title=Scorpion_II&action=edit§ion=3)] **"The Narmer Palette", The Ancient Egypt, retrieved ngày 19 tháng 9 năm 2007** [^](#cite_ref-1) **Krzysztof Marek Ciałowicz:** [^](#cite_ref-2) *La Naissance d'un Royaume:. L'Egypte des la periode prédynastique à la fin de la Ière Dynastie*Inst. Archeologii Uniw. Jagiellońskiego, Kraków 2001, ISBN 83-7188-483-4, p. 97 & 98. **Werner Kaiser, Günter Dreyer: Umm el-Qaab: Nachuntersuchungen im frühzeitlichen Königsfriedhof. 2. Vorbericht. Trong: MDAIK Nr. 38. von Zabern, Mainz 1982, ISBN 3-8053-0552-4, p.70.** [^](#cite_ref-3) **Krzysztof Marek Ciałowicz:** [^](#cite_ref-4) *La Naissance d'un Royaume:. L'Egypte des la periode prédynastique à la fin de la Ière Dynastie*Inst. Archeologii Uniw. Jagiellońskiego, Kraków 2001, ISBN 83-7188-483-4, p. 97 & 98.

X-Cache: cp1053 miss, cp1065 miss


text:
Hiển thị việc làms 1 - 10 trong tổng số 629
Nhân Viên Marketing OnlineCông Ty TNHH Sản Xuất Thương Mại Dịch Vụ Nội Thất Gia Phát - Thành phố Hồ Chí Minh, Hồ Chí MinhCó kinh nghiệm ít nhất 1 năm về SEO, Marketing Online; Có kỹ năng quản lí thời gian, quản lí công việc đúng tiến độ, kỹ năng giải quyết vấn đề; Ý thức trách...
Nhân Viên Kinh Doanh Online Biết Ngoại NgữCÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí MinhChúng tôi cùng sáng tạo, kết nối & tăng thêm giá trị cho các nhà sáng tạo nội dung Online....
Việc Làm Thêm Online Buổi Tối Tại Nhà Lương Cao 5-7 triệu/thángThành phố Hồ Chí Minh, Hồ Chí Minhcho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn làm việc. Việc của bạn là chia sẻ Tin, chỉ cần làm việc theo hướng dẫn thế là hoàn thành...Nộp đơn nhanh
Việc Làm Ngoài Giờ Cho Nhân Viên Văn Phòng 3h/Ngay Lương CaoTUYỂN NHÂN VIÊN LÀM THÊM TẠI NHÀ - Hồ Chí Minhbạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn làm việc. Việc của bạn là chia sẻ Tin...
Việc Làm Thêm Tại Nhà Buổi Tối Chỉ 2h-3h/ngày Lương Cao 5-7 triệu/tháng.vieclamthem2603 - An Tây, Hồ Chí Minhbạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn làm việc. Việc của bạn là chia sẻ Tin...
Việc Làm Thêm Tại Nhà Cho Sinh Viên chỉ 3h/ngày-Lương Cao 6 triệu/thángvieclamthem2603 - Cần Thơ, Cần Thơbạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn làm việc. Việc của bạn là chia sẻ Tin...
Việc Làm Thêm Tại Nhà Cho Nhân Viên Văn Phòng 3h/Ngay Lương 6-8 Triệu/thángThành phố Hồ Chí Minh, Hồ Chí MinhCông việc dành cho người nội trợ, sinh viên, nhân viên văn phòng, lao động phổ thông có nhu cầu làm them tại nhà từ 2-3h/ngày hoặc nhiều hơn…phù hợp với tất cả...
Việc làm thêm tại nhà cho người có máy tính lương caoÝ TƯỞNG - Cần Thơ, Cần ThơMô tả công việc TUYỂN DỤNG GẤP NHÂN VIÊN LÀM TẠI NHÀ Công việc dành cho người nội trợ, sinh viên, nhân viên văn phòng, lao động phổ thông có nhu cầu làm them...
Việc làm thêm tại nhà cho người nội trợThành phố Hồ Chí Minh, Hồ Chí MinhBạn phải đến công ty 1 lần để được hướng dẫn công việc và lương rõ ràng, cụ thể trong vòng 20 Phút. Sau đó về nhà làm, ko làm tại Công Ty, ko cần đến Công Ty...Nộp đơn nhanh
Việc Làm Thêm Tại Nhà Tại TPHCM - Lương 6-8 Triệu/thángThành phố Hồ Chí Minh, Hồ Chí Minhcho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn làm việc. Việc của bạn là chia sẻ Tin, chỉ cần làm việc theo hướng dẫn thế là hoàn thành...
Công tác viên viết bàiVIỆC LÀM THÊM TẠI NHÀ CHO HỌC SINH – SINH VIÊN - Thành phố Hồ Chí Minh, Hồ Chí Minh+ Vị trí: Cộng tác viên viết bài - Công việc online làm việc tại nhà. Phù hợp với các đối tượng có máy tính, học sinh, sinh viên, người lao động, có nhiều thời...
Việc Làm Online Tại Nhà Lương Cao Lương 6-8 triệu/tháng, Không Cần Kinh NghiệmBà Rịa-Vũng TàuCông việc dành cho người có nhu cầu làm thêm tại nhà, làm bán thời gian, làm ngoài giờ, làm buổi tối,… Quyền Lợi: ...Nộp đơn nhanh
Nhân Viên Kinh Doanh Online Biết Tiếng Ấn ĐộCÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí MinhTìm kiếm khách hàng/đối tác online tại Việt Nam & Ấn Độ Tư vấn, đàm phán và ký kết hợp đồng Duy trì & phát triển các mối quan hệ khách hàng Chăm sóc khách...
Nhân Viên Kinh Doanh Online Biết Tiếng Tây Ban NhaCÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí MinhThành thạo tiếng Tây Ban Nha (nghe, nói, đọc, viết)....
SEO/ Sales MarketingCty TNHH TM Đầu Tư DV Bất Động Sản Gia Phát - Thành phố Hồ Chí Minh, Hồ Chí MinhĐam mê về SEO/Marketing Online Có các kiến thức căn bản về SEO Chăm chỉ, chịu khó, làm việc ĐÚNG Deadline Ai chưa có kinh nghiệm thực chiến thì sẽ được đào tạo...
Tạo thông báo việc làm
Bạn có thể huỷ thông báo việc làm bất cứ lúc nào.
Lưu việc làm để truy cập chúng từ mọi nơi.
Đang đăng nhập...
Đang cập nhật lại...
Không bỏ lỡ việc làm nào. Nhận việc làm mới hằng ngày.
Tạo thông báo việc làm
Bạn có thể huỷ thông báo việc làm bất cứ lúc nào.

markdown:
Hiển thị việc làms
**1 - 10**trong tổng số **629**
## Công Ty TNHH Sản Xuất Thương Mại Dịch Vụ Nội Thất Gia Phát - Thành phố Hồ Chí Minh, Hồ Chí Minh
[Nhân Viên Marketing](/job/rd/69cfa00f184943582b255160bcf346a2?sp=sserp_top&sponsored=true&sr=1&tk=87aef406-3760-473c-8c3f-882c29c07817) **Online**Có kinh nghiệm ít nhất 1 năm về SEO, Marketing **Online**; Có kỹ năng quản lí thời gian, quản lí công **việc**đúng tiến độ, kỹ năng giải quyết vấn đề; Ý thức trách...
## CÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí Minh
[Nhân Viên Kinh Doanh](/job/rd/1cf6b33cd198a169a30a23b3ab02354d?sp=sserp_top&sponsored=true&sr=2&tk=87aef406-3760-473c-8c3f-882c29c07817) **Online**Biết Ngoại NgữChúng tôi cùng sáng tạo, kết nối & tăng **thêm**giá trị cho các **nhà**sáng tạo nội dung **Online**....
## Thành phố Hồ Chí Minh, Hồ Chí Minh
**Việc** **Làm** **Thêm** **Online**Buổi Tối **Tại** **Nhà**Lương Cao 5-7 triệu/thángcho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn **làm** **việc**. **Việc**của bạn là chia sẻ Tin, chỉ cần **làm** **việc**theo hướng dẫn thế là hoàn thành...Nộp đơn nhanh
## TUYỂN NHÂN VIÊN
**Việc** **Làm**Ngoài Giờ Cho Nhân Viên Văn Phòng 3h/Ngay Lương Cao **LÀM** **THÊM** **TẠI** **NHÀ**- Hồ Chí Minhbạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn **làm** **việc**. **Việc**của bạn là chia sẻ Tin...
## vieclamthem2603 - An Tây, Hồ Chí Minh
**Việc** **Làm** **Thêm** **Tại** **Nhà**Buổi Tối Chỉ 2h-3h/ngày Lương Cao 5-7 triệu/tháng.bạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn **làm** **việc**. **Việc**của bạn là chia sẻ Tin...
## vieclamthem2603 - Cần Thơ, Cần Thơ
**Việc** **Làm** **Thêm** **Tại** **Nhà**Cho Sinh Viên chỉ 3h/ngày-Lương Cao 6 triệu/thángbạn. Chia sẽ các Tin, Hình ảnh, Nội dung, các Sự kiện cho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn **làm** **việc**. **Việc**của bạn là chia sẻ Tin...
## Thành phố Hồ Chí Minh, Hồ Chí Minh
**Việc** **Làm** **Thêm** **Tại** **Nhà**Cho Nhân Viên Văn Phòng 3h/Ngay Lương 6-8 Triệu/thángCông **việc**dành cho người nội trợ, sinh viên, nhân viên văn phòng, lao động phổ thông có nhu cầu **làm** **them** **tại** **nhà**từ 2-3h/ngày hoặc nhiều hơn…phù hợp với tất cả...
## Ý TƯỞNG - Cần Thơ, Cần Thơ
**Việc** **làm** **thêm** **tại** **nhà**cho người có máy tính lương caoMô tả công **việc**TUYỂN DỤNG GẤP NHÂN VIÊN **LÀM** **TẠI** **NHÀ**Công **việc**dành cho người nội trợ, sinh viên, nhân viên văn phòng, lao động phổ thông có nhu cầu **làm** **them**...
## Thành phố Hồ Chí Minh, Hồ Chí Minh
**Việc** **làm** **thêm** **tại** **nhà**cho người nội trợBạn phải đến công ty 1 lần để được hướng dẫn công **việc**và lương rõ ràng, cụ thể trong vòng 20 Phút. Sau đó về **nhà** **làm**, ko **làm** **tại**Công Ty, ko cần đến Công Ty...Nộp đơn nhanh
## Thành phố Hồ Chí Minh, Hồ Chí Minh
**Việc** **Làm** **Thêm** **Tại** **Nhà** **Tại**TPHCM - Lương 6-8 Triệu/thángcho Công ty. Công Ty sẽ cung cấp sẵn các Group, Hội và Diễn Đàn để bạn **làm** **việc**. **Việc**của bạn là chia sẻ Tin, chỉ cần **làm** **việc**theo hướng dẫn thế là hoàn thành... [Công tác viên viết bài](/job/rd/1311836c19bb5247c77e1db9248f6d42?sp=serp&sponsored=false&sr=9&tk=87aef406-3760-473c-8c3f-882c29c07817) **VIỆC** **LÀM** **THÊM** **TẠI** **NHÀ**CHO HỌC SINH – SINH VIÊN - Thành phố Hồ Chí Minh, Hồ Chí Minh+ Vị trí: Cộng tác viên viết bài - Công **việc** **online** **làm** **việc** **tại** **nhà**. Phù hợp với các đối tượng có máy tính, học sinh, sinh viên, người lao động, có nhiều thời...
## Bà Rịa-Vũng Tàu
**Việc** **Làm** **Online** **Tại** **Nhà**Lương Cao Lương 6-8 triệu/tháng, Không Cần Kinh NghiệmCông **việc**dành cho người có nhu cầu **làm** **thêm** **tại** **nhà**, **làm**bán thời gian, **làm**ngoài giờ, **làm**buổi tối,… Quyền Lợi: ...Nộp đơn nhanh
## CÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí Minh
[Nhân Viên Kinh Doanh](/job/rd/7f0279ad344b5c16fd066c4d63c4facb?sp=sserp_bottom&sponsored=true&sr=3&tk=87aef406-3760-473c-8c3f-882c29c07817) **Online**Biết Tiếng Ấn ĐộTìm kiếm khách hàng/đối tác **online** **tại**Việt Nam & Ấn Độ Tư vấn, đàm phán và ký kết hợp đồng Duy trì & phát triển các mối quan hệ khách hàng Chăm sóc khách...
## CÔNG TY CỔ PHẦN PHÁT TRIỂN THƯƠNG HIỆU ĐẠI SỨ TRẺ - Thành phố Hồ Chí Minh, Hồ Chí Minh
[Nhân Viên Kinh Doanh](/job/rd/e8953dfd141aec8d0933c8fb1d33e231?sp=sserp_bottom&sponsored=true&sr=4&tk=87aef406-3760-473c-8c3f-882c29c07817) **Online**Biết Tiếng Tây Ban **Nha**Thành thạo tiếng Tây Ban **Nha**(nghe, nói, đọc, viết)....
## Cty TNHH TM Đầu Tư DV Bất Động Sản Gia Phát - Thành phố Hồ Chí Minh, Hồ Chí Minh
[SEO/ Sales Marketing](/job/rd/75e6b7b67ebfb30e081142cda7ab25ed?sp=sserp_bottom&sponsored=true&sr=5&tk=87aef406-3760-473c-8c3f-882c29c07817)Đam mê về SEO/Marketing **Online**Có các kiến thức căn bản về SEO Chăm chỉ, chịu khó, **làm** **việc**ĐÚNG Deadline Ai chưa có kinh nghiệm thực chiến thì sẽ được đào tạo...
Tạo thông báo việc làm
Bạn có thể huỷ thông báo việc làm bất cứ lúc nào.
Lưu việc làm để truy cập chúng từ mọi nơi.
Đang đăng nhập...
Đang cập nhật lại...
Không bỏ lỡ việc làm nào. Nhận việc làm mới hằng ngày.
Tạo thông báo việc làm
Bạn có thể huỷ thông báo việc làm bất cứ lúc nào.

WARC-Truncated: length

X-XSS-Protection: 1; mode=block

Connection: Close

Server: nginx

Cache-Control: max-age=0, private, must-revalidate

X-Frame-Options: SAMEORIGIN

Content-Type: text/html; charset=utf-8


text:
-
Agoda PointsMAX!
- cùng chương trình, nhiều điểm hơn
1
Chọn chương trình thành viên
PointsMAX
Ngôn ngữ
Chương trình thành viên A
Chương trình thành viên B
Trong menu, nhấp PointsMAX và chọn chương trình thành viên yêu thích của bạn.
2
Chọn điểm ưu đãi
Phòng khách sạn A
Thông tin phòng
Tích lũy5000 điểm
Chọn loại phòng và điểm cho khách sạn bạn đã chọn.
3
Nhập mã số thành viên
Nước cấp hộ chiếu
Mã số thành viên chương trình
1234
Điền số thẻ thành viên của chương trình đã chọn khi đặt phòng. Số điểm sẽ được cộng vào tài khoản của bạn sau khi trả phòng.
Bắt đầu ở đây và chọn chương trình yêu thích của bạn:

markdown:
-
## Agoda PointsMAX!
- cùng chương trình, nhiều điểm hơn
1
#### Chọn chương trình thành viên
PointsMAX
Ngôn ngữ
Chương trình thành viên A
![ Chương trình thành viên A](https://cdn6.agoda.net/images/abtest/PRIUS/icon/icon-pointer@2x.png)
Chương trình thành viên B
Trong menu, nhấp PointsMAX và chọn chương trình thành viên yêu thích của bạn.
2
#### Chọn điểm ưu đãi
![ Chọn điểm ưu đãi](https://cdn6.agoda.net/images/abtest/PRIUS/icon/icon-bed.png)
Phòng khách sạn A
Thông tin phòng
Tích lũy5000 điểm
Chọn loại phòng và điểm cho khách sạn bạn đã chọn.
3
#### Nhập mã số thành viên
Nước cấp hộ chiếu
Mã số thành viên chương trình
1234
Điền số thẻ thành viên của chương trình đã chọn khi đặt phòng. Số điểm sẽ được cộng vào tài khoản của bạn sau khi trả phòng.
Bắt đầu ở đây và chọn chương trình yêu thích của bạn:

Access-Control-Allow-Credentials: true

Cache-Control: private

X-Origin: ashburn

X-Recruiting: Like HTTP headers? Come write ours: http://grnh.se/1qxadk

Access-Control-Allow-Methods: GET,POST

Access-Control-Allow-Headers: Content-Type

Vary: User-Agent, Accept-Encoding