哲学家进餐问题 java

哲学家进餐问题的解决方案主要有以下几种：
（１） 利用ＡＮＤ 型信号量机制．该方案的思路是，仅当哲学家左右两支筷子都空闲时，才允许他拿起筷子进餐，即哲学家所需要的临界资源──筷子，要么两支全部分配给他，要么一支都不分配，这样就保证了总有哲学家能同时拿到两支筷子而进餐，当他进餐完毕释放筷子后，其他哲学家也可以顺利地运行下去，避免了死锁的产生．
（２） 对哲学家按序号进行区分．该方案的思路是，让第０、２、４ 号哲学家先去申请他们左手边的筷子（即第０、２、４ 号筷子），然后再去申请右手边的筷子，让第１、３ 号哲学家先申请他们右手边的筷子（即第２、４ 号筷子），然后再申请左手边的筷子．这样总会有一名哲学家能够同时拿到两支筷子而进餐，当他进餐完毕，释放其左右手的筷子后，其他哲学家又能继续下去，从而确保每位哲学家都可以顺利地进餐．
（３） 最多允许４ 名哲学家提出申请．该方案的思路是，至多允许４ 名哲学家提出进餐申请，以保证至少有１ 名哲学家能够拿到两支筷子而进餐，他最终总会释放出所使用的两支筷子，从而使其余哲学家可以进餐．
（4）回退思想的引入回退机制的理论依据是处理死锁基本方法中的预防死锁策略．预防死锁是指通过设置某些限制条件，去破坏产生死锁的４ 个必要条件中的一个或几个来防止死锁的发生．其中“摒弃不剥夺条件”规定，当一个进程提出新的资源请求而不能立即得到满足时，必须释放其已经保持了的所有资源，即已经占有的资源可以被剥夺．根据上面的理论，本文解决哲学家进餐问题的基本思路是，让每名哲学家先去申请他左手边的筷子，然后再申请他右手边的筷子，如果右手边的筷子不空闲，则比较当前哲学家i 和他右手边的哲学家（i ＋１）％５，看谁取得各自左手边筷子的时间更晚，令其回退（即释放左手筷子，再重新申请左手筷子），直到此哲学家右手边的筷子空闲为止．通过设置回退机制，可以确保每位哲学家都能顺利进餐．

同步和死锁的关系要搞清楚：

同步是为了保护多线程对共享数据的访问，消除数据腐蚀。同步的过程中可能会产生死锁！

也就是说，会产生死锁的程序中，共享数据得到了保护，只是程序会死锁。

我的方案：最后一个人先拿左筷，其他人都先拿右筷。（破坏死锁链）
/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package tr52_java;

import java.util.Random;
import java.util.logging.Level;
import java.util.logging.Logger;

public class Philosopher extends Thread {

    private static int MAX_PHILO = 4;
    private int num;
    private ChopStick right, left;
    private boolean finished = false;
    private Random rand = new Random();
    private boolean flag = true;

    public Philosopher(int i, ChopStick r, ChopStick l) {
        num = i;
        right = r;
        left = l;
        start();
    }

    public void pause() {
        try {
            sleep(rand.nextInt(1000));
        } catch (Exception e) {
            e.printStackTrace();
        }
    }

//会死锁！死锁点在synchronized(left)
//    @Override
//    public void run() {
//        while (!finished) {
//            flag = true;
//            synchronized (right) {
//                while (!right.isFree()) {
//                    try {
//                        right.wait();
//                    } catch (InterruptedException ex) {
//                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
//                    }
//                }
//                pause();
//                synchronized (left) {
//                    while (!left.isFree()) {
//                        flag = false;
//                        right.notify();
//                        System.out.println(num + "is thinking");
//                        break;
//                    }
//                    if (flag) {
//                        right.take();
//                        System.out.println(num + ": right taking");
//                        pause();
//
//                        left.take();
//                        System.out.println(num + ": left taking");
//                        pause();
//
//                        System.out.println(num + ": eating");
//                       
//                        right.release();
//                        right.notifyAll();
//                        System.out.println(num + ": right releasing");
//                        pause();
//
//                        left.release();
//                        left.notifyAll();
//                        System.out.println(num + ": left releasing");
//                        pause();
//                    }
//                }
//            }
//        }
//    }
    @Override
    public void run() {
        while (!finished) {
            System.out.println(num + "is thinking");
            synchronized (right) {
                while (!right.isFree()) {
                    try {
                        right.wait();
                    } catch (InterruptedException ex) {
                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
                    }
                }
                right.take();
                System.out.println(num + ": right taking");
                pause();
            }

            synchronized (left) {
                while (!left.isFree()) {
                    try {
                        left.wait();
                    } catch (InterruptedException ex) {
                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
                    }
                }
                left.take();
                System.out.println(num + ": left taking");
                pause();
            }

            System.out.println(num + ": eating");
           
            synchronized (right) {
                right.release();
                right.notifyAll();
                System.out.println(num + ": right releasing");
                pause();
            }

            synchronized (left) {
                left.release();
                left.notifyAll();
                System.out.println(num + ": left releasing");
                pause();
            }
        }
    }

//    @Override
//    public void run() {
//        while (!finished) {
//            right.take();
//            pause();
//            left.take();
//            pause();
//            left.release();
//            pause();
//            right.release();
//            pause();
//        }
//    }
public static void main(String[] args) {
        ChopStick[] chopStick = new ChopStick[MAX_PHILO];
        for (int i = 0; i < MAX_PHILO; i++) {
            chopStick[i] = new ChopStick(i);
        }

        Philosopher[] phil = new Philosopher[MAX_PHILO];
        for (int i = 0; i < MAX_PHILO; i++) {
            if (i < MAX_PHILO - 1) {
                phil[i] = new Philosopher(i, chopStick[i], chopStick[i > 0 ? i - 1 : MAX_PHILO - 1]);
            } else {
                phil[i] = new Philosopher(i, chopStick[i - 1], chopStick[i]);
           





}
        }
    }
}

class ChopStick {

    private int num;
    private boolean free = true;

    public ChopStick(int i) {
        num = i;
    }

//方案1：
    public void take() {
        free = false;
    }

    public boolean isFree() {
        return free;
    }

    public void release() {
        free = true;
    }
//    public synchronized void take() {
//        free = false;
//    }
//
//    public boolean isFree() {
//        return free;
//    }
//
//    public synchronized void release() {
//        free = true;
//    }
}

(转载）用latex和beamer做幻灯片

 原文地址：http://xiang.blog.edu.cn/2008/157618.html
做幻灯片是一件头疼的事。而用latex做幻灯片是一件很头疼、很头疼、cdots、很头疼的事……总结和收集了一些经验如下：

• beamer教程
  有很多教程。对于初学者，最好先copy别人（比如师兄师姐的）模板用，或者直接看beamer的例子，C:CTeXtexmfdoclatexbeamerexamples。入门后，我觉得最好的提高教程是Ki-Joo Kim的Beamer v3.0 Guide，本身就是一个幻灯片，写的很清楚，看得也很爽。最后是beamer的用户手册，参考用。

• 中文幻灯片
  一定要定义documentclass[cjk]{beamer}，别忘了“cjk”，否则编译不通过

• pdf书签中文乱码
  这是做中文幻灯片时必然遇到的问题……
  
  在Adobe Reader中，显示在一旁的书签(Bookmark)是Unicode的。这样一来，如果单纯是使用pdflatex生成pdf将会显示乱码。所以，若要生成中文的Bookmark就需要执行如下命令:
  
  pdflatex slide.tex
  pdflatex slide.tex
  gbk2uni slide.out
  pdflatex slide.tex
  
  注：gbk2uni是cct的一个小工具。

• 改变文字颜色
  textcolor{blue!80!white}可以调色，这是xcolor包的一个功能。
  在WinEdt中要查看任何一个package的用户手册，可以在菜单中选Help-Latex doc，然后输入包名即可。

• lyx：可见即所得的Latex编辑器
  每个 frame里几乎都要敲一遍begin{itemize}end{itemize；思考若干秒后决定再敲一遍（因为要缩进其中的几个item）；再思考若 干秒后把刚敲的这两行删掉（取消缩进）……用beamer就是这么痛苦。想想powerpoint，只要按Tab和Shift+Tab……于是我装了Lyx。虽然它其实还是很难用。下面是Lyx的几个经验：
  • 导入中文latex源文件前，应在latex源文件中写usepackage[gbk]{inputenc}指定编码，否则导入后是乱码
  • Document-preferences-language改为中文，否则查看源码时有很多解码错误
  • 总的来说，还是不建议用Lyx，没有想像中得那么好。

• WinEdt宏
  为了从上面描述的重复劳动中解脱出来，我花了点时间看了看WinEdt的宏语言手册，写了几个简单的宏，发现还是挺好用的。
  
  
  • 为当前选中的文本增加一层itemize环境： BeginGroup;
    GetSel(0,1);
    CMD("Delete");
    Ins("begin{itemize}");
    NewLine;
    Ins("%!1");
    NewLine;
    Ins("end{itemize}");
    NewLine;
    EndGroup;
    
    原理很简单，把当前选中文本保存到变量%!1中，删除当前文本，然后插入适当的文本。
    
  • 删除当前选中文本最外层的itemize环境：
    
    DelLabel("","begin{itemize}","end{itemize}");
    就这一行。注意，一定要保证当前选中的文本中的头尾刚好是一对begin{itemize}和end{itemize}。
    
  • 自动插入任意的环境
    
    GetString("Input environment name:","Surround By"); // input string is saved in %!?
    BeginGroup;
    GetSel(0,1); // save current selection in %!1
    CMD("Delete");
    Ins("begin{%!?}");
    NewLine;
    Ins("%!1");
    NewLine;
    Ins("end{%!?}");
    IfStr('%!1','','=', "CMD('Line Up')", 'Relax'); // move one line up if current selection is empty (i.e. inserting a new environment)
    EndGroup;
    
    这个宏首先会提示你输入环境名，然后自动在当前选中的文本前后插入begin{xxx}和end{xxx}。
    
  • 安装宏的方法
    
    Help-Macro Manual，第一页就讲了这个，配了图，可能比我说的更清楚。不过这里还是大致说一下：首先把上面几个宏分别保存为.edt类型的文件，复制到 WinEdt文件夹下面，例如C:CTeXWinEdtMacros。然后在Options-Menu setup-Popup menus里面，选择左边的“Edit”一项，然后按上面的第二个按钮，出现新的对话框，在这里可以修改右键弹出菜单的内容，再按最上面第二个按钮，选 Macro，这样就添加了一个菜单项，给它起个名字”Insert Environment“，然后在Macro编辑框中输入[Exe('%bMacrosInsert Environment.edt');]，确定后即可在右键弹出菜单里用这个新命令了。安装其他宏的方法类似。

总结：自己动手，丰衣足食。其实早就该学一下WinEdt的这些高级功能，可以节约不少时间……

（转载）软件模型检测简介

 原文地址：http://blog.csdn.net/xander1981/archive/2009/10/10/4650092.aspx

1.      什么是软件模型检测（software model checking）

a)         软件模型检测是用来在程序执行过程中证明性质正确性的算法。它源于逻辑和定理证明，这两者都给出了基础问题形式化的基本概念，以及提供了分析逻辑问题的算法流程。

b)        随 着软件规模的越来越大，使得人工的验证软件变得越来越难，而且人工的验证本身是否可靠也是一个很大的问题。因此，软件模型检测研究的目的就是扩展自动验证 技术的应用领域，将其用于程序的推理，无论是在程序处理的验证还是性质的验证上，都要最大程度的增加自动化的比例，从而减轻人，尤其是专家程序员的工作 量。

2.      软件模型检测的发展

    软件模型检测目前有三方面的发展，这三方面是同时发展的，有其各自的特点：

a)         程序逻辑和相关判定过程【Nelson 1981; Nelson and Oppen 1980; Shostak 1984】的发展给无限状态过程的推理提供了基本框架和基础算法。

b)        基于时序逻辑【Pnueli 1977; Emerson 1990】的自动化模型检测技术【Clarke and Emerson 1981; Queille and Sifakis 1981; Vardi and Wolper 1994】的发展为解决状态爆炸问题提供了基础算法。

c)        通过抽象解释对编译器进行分析和形式化，使得我们在无限状态的逻辑世界空间和有穷状态的算法世界之间建立起了很好的联系。

80年代到90年 代期间，这三方面虽然各自有其发展，但是，之间的相互联系却很少。直到最近十几年，现代化的软件模型检测工具成为了研究领域的研究重点，上述三方面的研究 也慢慢的结合到了一起。严格意义上来说，“软件模型检测工具”的说法是不太恰当的，因为当前的工具同时具备了定理证明、模型检测、数据流分析等多种传统意 义上的程序分析方法。我们保留这一说法的目的是为了反映一个阶段历史的发展。

3.      有形枚举的模型检测（concrete enumerative model checking）

a)         有形（concrete）：方法只关心程序的状态。

b)        枚举（enumerative）：方法的操作对象是程序的单个状态。而符号化（symbolic）的模型检测操作的是状态的集合。

c)        有形枚举的模型检测来源于70年代末期的测试和仿真技术，尤其是对网络协议的测试技术（同一时期，还产生了对时序逻辑进行声明的技术）。之后，该方法被成功的应用在了异步信息传输协议、cache一致性协议等多个领域。

d)        方法介绍：该方法是基于对状态图的搜索遍历，找出所有可达状态的集合，再检查看错误状态是否包含在可达状态集合当中，如果是，则说明系统不安全。否则，说明系统是安全的。

e)         代表性的工具：SPIN【Holzmann 1997】和MURPHI【Dill 1996】。

f)         存在问题：状态爆炸！！！

g)        解决方法：

                         i.              基于削减的技术（reduction-based techniques）：找出程序行为中的等价关系，并且只考虑每个等价类中的一个成员，保证削减后的是完备的，也即原系统中有的bug，在削减后的系统中同样存在。主要的削减技术有——偏序削减（partial-order reduction）【Valmari 1992; Katz and Peled 1992; Godefroid 1996】，对称削减（symmetry reduction）【Clarke et al. 1993; Emerson and Sistla 1996; Ip and Dill 1996; Sistla et al. 2000】，基于模拟和互模拟的等价类划分来最小化系统【Bouajjani et al. 1990; Loiseaux et al. 1995; Bustan and Grumberg 2003】。

                       ii.              合成技术（compositional techniques）：将原始的验证问题分解成对其子问题的安全性验证，由子问题安全可以推导出原问题安全。假设-保证推理（assume-guarantee reasoning）【Misra and Chandy 1981; Jones 1983; Stark 1985; Abadi and Lamport 1993; Abadi and Lamport 1995; Henzinger et al. 1998; Alur and Henzinger 1999】是合成推理中发展得比较好的技术。其中还用到了一些启发式的搜索技术来加快对状态空间的搜索，快速的找到系统的问题所在，例如重复加深算法（iterative deepening）【Korf 1985】、最好-优先搜索（best-first search）【Russell and Norvig 2003】、A*算法【Hart et al. 1968; Russell and Norvig 2003】。这些方法在MURPHI和SPIN中也都有了很好的应用。

h)        少量状态搜索（stateless search）

                         i.              基于深度的限界模型检测。当某一深度的执行路径全部探测完以后没有发现错误就增加深度，再重复这一过程，直到返回UNSAFE，表明发现了与待验证的安全性性质相冲突的执行。该算法的主要特点就是对待分析的程序的表示要求不是很高。我们只要做到两点就可以了：

1.         重置（reset）：对程序的初始状态进行重置；

2.         执行（execute）：在相应的调度策略下执行。

i)          基于执行的工具：

                         i.              Verisoft：最早使用基于执行的少量状态搜索的模型检测软件。能对若干通过消息队列进行通讯的Unix进程进行检测。

                       ii.              JavaPathFinder：对Java程序的模型检测工具。加入了许多常用的基于削减的技术来解决状态爆炸的问题。同时有多种启发式方法来搜索存储的状态空间以及使用一些技术来获得一个更高的覆盖率。

                      iii.              CMC：可以检测C语言程序在执行时，OS层级的调度。

                     iv.              MaceMC：用于检测分布式系统。

                       v.              Chess：用于检测多线程的Windows程序。

4.      有形符号化的模型检测（concrete symbolic model checking）

a)         基 于枚举的模型检测技术受到状态和迁移关系数量的影响很明显，很容易产生状态爆炸的问题，因此在实际应用中会遇到很多的困难。这就使得研究者们把目光放在了 符号化的模型检测算法上。符号化的模型检测方法是以状态集合为操作对象的，而不是单个单个的状态。符号化的表示方法能够更加简洁的表示系统的状态，而且也 能够更好的表示无限状态的集合。为了能够进行验证，符号化的表示方法所表示出来的状态集合还要能够支持必要的运算操作，例如求状态集合的后继、前驱，状态 集合的合并等等。

b)        符号化的模型检测算法的基本搜索过程和枚举的模型检测算法的搜索过程类似，只是我们现在操作的对象是状态集合（或者说是区域，region）而不是单个独立的状态。符号化的模型检测方法之所以有效的另外一个原因就是有强有力的可满足性求解工具作其后盾，如SAT【Silva and Sakallah 1996; Moskewicz et al. 2001; Een and Sorensson 2003】，BDD【Bryant 1986; Somenzi 1998】，以及SMT【Dutertre and Moura; Bruttomesso et al. 2008; de Moura and Bjørner 2008】。

c)        符号化的表示方法

                         i.              命题逻辑：SAT，BDD。

                       ii.              带有解释定理的一阶逻辑：SMT。

d)        限界模型检测【Biere et al. 1999】

                         i.              有限步的展开程序控制流程图，检查在该步数内能够找到错误状态，若找到，则返回系统不安全的信息，若找不到，则增加步数，直到步数到达上界，此时返回找不到错误状态的信息。

                       ii.              对软件的限界模型检测工具又可以分为两类：

1.         用命题逻辑生成约束，通过SAT求解器来求解：CBMC【Kroening et al.2003】，F-Soft【Ivancic et al. 2008】，Saturn【Xie and Aiken 2005】，Calysto【Babic and Hu 2008】。

2.         用适当的一阶理论来生成约束，用SMT求解器来求解。

                      iii.              限界模型检测适合于查错，即在规定步数内找到系统的错误状态。若系统是安全的，则限界模型检测无法给出完备的判定。我们可以采用其它的方法来解决对系统安全性的判定，如k-induction【Sheeran et al. 2000; de Moura and Ruess 2003】。k-induction是假设归纳不变式在程序执行路径前k步都是成立的，然后证明该不变式在k+1步时同样成立。其中，长度为k的路径是按照限界模型检测的方法进行编码的。这种基于不变式的约束式求解方法受到两方面的限制：1.要猜测出正确的不变式；2.方法的效率受制于求解非线性算术表达式的求解器的效率。因此，这种方法目前只适用于规模较小的程序的验证。

5.      模型检测和抽象技术

a)         对于无限状态的程序来说，符号化的可达性分析同样不能终止，或者是说要花费难以估量的时间和空间代价才有可能终止。抽象模型检测的可达性分析是在抽象域的基础上进行的，而抽象域则是通过抽象语义对程序的运行进行适当的信息捕获而得到的【Cousot and Cousot 1977】。好的抽象域和抽象语义的选择可以很好的保证算法的可靠性和有效性。

b)        基于抽象的可达状态分析

该算法和符号化的可达状态分析算法类似，只是用抽象域代替了符号化的状态集合。根据抽象对象的不同，也有不同的抽象方法：

1.         谓词抽象：【Agerwala and Misra 1978; Graf and Saïdi 1997; Saïdi and Shankar 1999; Das et al. 1999】，代表工具：SLAM，BLAST【Beyer et al. 2007a】。Cartesian谓词抽象技术【Ball et al. 2001】是其中的代表，在系统开销和求解效率上取得了很好的平衡，并且在SLAM中关于C程序验证的部分有其相关的使用，叫做c2bp【Ball et al. 2001】。

2.         控制抽象：流敏感，流不敏感，路径敏感等【Beyer et al. 2007b】。主要是针对非递归的并发程序进行抽象，抽象成顺序执行的程序进行验证【Dwyer and Clarke 1994】。代表工具：MAGIC【Chaki et al. 2004】。

3.         各种抽象技术相结合：结合多种抽象技术，对系统的不同性质进行抽象爱那个，得到一个更加强大的分析工具。代表工具：F-Soft【Jain et al. 2006】，IMPACT【McMillan 2006】，Astree analysis tool【Blanchet et al. 2002; Blanchet et al. 2003】，BLAST。

若基于抽象的可达性分析算法返回safe，则表示原系统真的是安全的；若返回unsafe，则无法判定原系统到底是safe还是unsafe的，因为在抽象的过程中省略掉了一部分信息，有可能原系统是安全的，而在抽象后的系统中却形成伪反例（不完备）。这就需要根据某些信息对抽象后的系统进行修正。基于反例的抽象修正（counterexample guided abstraction refinement）就是其中之一。

6.      抽象修正技术

a)         通 常来说，抽象的模型检测技术是可靠的，也即抽象系统是安全的可以推出原系统也是安全的，但是抽象的模型检测方法是不完备的，也即在原系统是安全的情况下， 抽象系统有可能会得到一个错误的反例。因此，我们需要判断哪些反例是真的，即在原系统中存在的，哪些反例是假的，即在原系统中不可能存在的。出现后一种情 况时，我们希望模型检测算法能够自动的修正，得到一个新的抽象域重新进行检测。这种修正有可能是基于找到的伪反例（counterexample-guided refinement）【Ball and Rajamani 2000b; Clarke et al. 2000; Saidi 2000】，也有可能是其它的策略，例如：局部削减（localization reduction）【Kurshan 1994; Alur et al. 1995】。

上图为CEGAR算法描述。算法不断的修正抽象域A，知道证明系统是正确的，或者找到真正的反例为止。

b)        反例和修正

                         i.              反例：一条程序执行路径，其第一个状态为系统的初始状态，最后一个状态为一个错误状态。表明程序可以执行到一个错误状态，也即系统安全的一个反例。

                       ii.              基于语法的修正

1.         一个简单的排出伪反例的方法是查找公式中的不可满足的核心（unsatisfiable core）。有很多方法可以找到这个公式的集合：

a)         用贪心算法找最小不可满足集合，SLAM中用到了该方法【Ball and Rajamani 2002a】；

b)        查询判定的产生过程，找到证明不可满足的那些约束，选择该证明中那些在叶子节点出现的原子公式即可。该方法在BLAST中有实现【Henzinger et al 2002】。

2.         另外一种基于语法的修正方法是计算路径的前驱，即从错误的状态开始，往前计算每一步的状态，并根据计算出的状态中的原子命题进行修正，直至到达初始状态【Namjoshi and Kurshan 2000】。该方法在F-Soft中有应用。

                      iii.              基于插值的修正

基于语法的修正，往往只关注程序表面的一些问题，而没有考虑其内在的联系。而基于插值的方法则不同，【Henzinger et al. 2004】利用Craig插值（Craig Interpolation）来查找能够反映程序内在联系的断言，来验证给定的安全性性质。

                     iv.              基于抽象-修正的模型检测工具

1.         SLAM【Ball and Rajamani 2002b】

2.         BLAST【Beyer et al. 2007a】

3.         MAGIC【Chaki et al. 2003】

4.         F-Soft【Ivancic et al. 2005】

PostgreSQL Java 连接 Tomcat下 JNDI ， FATAL: password authentication failed for user "" 报错 等问题

1） PostgresQL java 连接
import java.sql.*;

public class PostgresConnector {
 public static void main(String[] args) {
  try {
   Class.forName("org.postgresql.Driver");
   Connection conn = DriverManager.getConnection("jdbc:postgresql://localhost:5432/TableName","username","password");
   System.out.println(conn.isClosed());
   Statement stmt=conn.createStatement();
   ResultSet rs=stmt.executeQuery("SELECT * from batiment");
   while(rs.next())
   {
    System.out.println(rs.getString(1));
   }
   conn.close();
  }
  catch(Exception ex){
      ex.printStackTrace();
   System.out.println("error!");
  }
 }
}  



2)Tomcat下 JNDI

   
第一步、配置tomcat目录下/conf下的context.xml （或者是netbeans      web pages 下 META-INF 的context.xml)
<Context antiJARLocking="true" path="/setms">
    <Resource name="jdbc/setms" auth="Container" type="javax.sql.DataSource" maxActive="100" maxIdle="30" maxWait="10000" username="postgres" password="12345" driverClassName="org.postgresql.Driver" url="jdbc:postgresql://localhost:5432/setmanager_dev" />
</Context>
第二步、配置项目中/WEB-INF/下的web.xml
  <resource-ref>
    <res-ref-name>jdbc/setms</res-ref-name>
    <res-type>javax.sql.DataSource</res-type>
    <res-auth>Container</res-auth>
  </resource-ref>
第三步、测试数据源
 <%@page contentType="text/html" pageEncoding="UTF-8"%>
<!DOCTYPE html>
<%@page import="java.sql.*, javax.sql.*, javax.naming.*"%>
<html>
<head>
<title>Using a DataSource</title>
</head>
<body>
<h1>Using a DataSource</h1>
<%
    DataSource ds = null;
    Connection conn = null;
    ResultSet result = null;
    Statement stmt = null;
    ResultSetMetaData rsmd = null;
    try{
      Context context = new InitialContext();
      Context envCtx = (Context) context.lookup("java:comp/env");
      ds =  (DataSource)envCtx.lookup("jdbc/setms");
      if (ds != null) {
        conn = ds.getConnection();
        stmt = conn.createStatement();
        result = stmt.executeQuery("SELECT * FROM Personne");
       }
     }
     catch (SQLException e) {
        System.out.println("Error occurred " + e);
      }
      int columns=0;
      try {
        rsmd = result.getMetaData();
        columns = rsmd.getColumnCount();
      }
      catch (SQLException e) {
         System.out.println("Error occurred " + e);
      }
 %>
 <table width="90%" border="1">
   <tr>
   <% // write out the header cells containing the column labels
      try {
         for (int i=1; i<=columns; i++) {
              out.write("<th>" + rsmd.getColumnLabel(i) + "</th>");
         }
   %>
   </tr>
   <% // now write out one row for each entry in the database table
         while (result.next()) {
            out.write("<tr>");
            for (int i=1; i<=columns; i++) {
              out.write("<td>" + result.getString(i) + "</td>");
            }
            out.write("</tr>");
         }

         // close the connection, resultset, and the statement
         result.close();
         stmt.close();
         conn.close();
      } // end of the try block
      catch (SQLException e) {
         System.out.println("Error " + e);
      }
      // ensure everything is closed
    finally {
     try {
       if (stmt != null)
        stmt.close();
       }  catch (SQLException e) {}
       try {
        if (conn != null)
         conn.close();
        } catch (SQLException e) {}
    }

    %>
</table>
</body>
</html>

记得拷贝postgresql-9.0-801.jdbc4.jar 到WEB-INF  lib 下 或 tomcat目录下/lib下




name：指定Resource的JNDI的名字、
auth：指定管理Resource的Manager，它有两个值：Container 和Application，Container并表示有容器来创建Resource，Application表示有Web应用来创建和管理Resource、
type：指定Resource所属的Java类名、
maxActive：指定数据库连接池中处于活动状态的数据库连接的最大数目，取值为0，表示不受限制、
maxIdle：指定数据库连接池中处于空闲状态的数据库连接的最大数目，取值为0，表示不受限制、
maxWait：指定数据库连接池中的数据库连接处于空闲状态的最长时间(以毫秒为单位)，超过这一时间将会抛出异常，取值为-1，表示可以无限制等待、
username：指定连接数据库的用户名、
password：指定连接数据库的口令、
driverClassName：指定连接数据库的JDBC驱动程序、
url：指定连接数据库的URL、


  FATAL: password authentication failed for user "" 问题
是由于user 权限不够， 检查postgreSQL中的表是不是 相应user （默认是postgres）， 再一次检查context.xml中的user！

Ada

1. 首先下载gnat  和 gps http://libre.adacore.com/libre/download/  并安装
2. 开发环境：gps、adagide、netbeans（安装插件）

为sal 设置环境变量 SALPATH

1. 安装sal： 解压文件， 命令：  ./install.sh

2. 设置环境变量： export PATH="$/home/marstnt/sal-3.0/bin" 然后用export命令查看，之后，sal-sim就可以用了。不过会有提示：
  “WARNING: SALPATH is now called SALCONTEXTPATH.
WARNING: The environment variable SALCONTEXTPATH is undefined, assuming  "." (i.e., just the current directory). The SALCONTEXTPATH specifies which directories will be searched for SAL context files. This is NOT a problem, but if you want a different search path, then you need to set the environment variable SALCONTEXTPATH.
”

3. 其实可以忽略上一步，当sal安装好后直接在命令
export SALCONTEXTPATH=.:/home/marstnt/sal-3.0/bin/      （绿色部分要改！）
export PATH=$PATH:/home/marstnt/sal-3.0/bin/
但是在重启命令行终端后一切又会恢复到默认设置，为了之久化，我们需要在etc/bash.bashrc最后添加相同命令
 #sal
export SALCONTEXTPATH=.:/home/marstnt/sal-3.0/bin/
export PATH=$PATH:/home/marstnt/sal-3.0/bin/
重启命令终端！
这样就可以使用sal了

PS：获取root：  sudo su   退出root：exit

       sudo vim /etc/bash.bashrc  按i进入插入模式，在最后一行添加
       #sal
       export SALCONTEXTPATH=.:/home/marstnt/sal-3.0/bin/
       export PATH=$PATH:/home/marstnt/sal-3.0/bin/
       按ESC 再按：   在lastline 输入w   再输q（保存退出）